chore: use #lang lean4 instead of new_frontend

src/Lean/Elab/PreDefinition/Basic.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,7 @@ import Lean.Meta.AbstractNestedProofs
 import Lean.Elab.Term
 import Lean.Elab.DefView
 import Lean.Elab.PreDefinition.MkInhabitant
-new_frontend
+
 namespace Lean.Elab
 open Meta
 open Term

src/Lean/Elab/PreDefinition/Main.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,7 +7,6 @@ Authors: Leonardo de Moura
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural
 import Lean.Elab.PreDefinition.WF
-new_frontend
 namespace Lean.Elab
 open Meta
 open Term

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.AppBuilder
-new_frontend
 namespace Lean.Elab
 open Meta
 

src/Lean/Elab/PreDefinition/Structural.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.ForEachExpr
 import Lean.Meta.RecursorInfo
 import Lean.Meta.Match.Match
 import Lean.Elab.PreDefinition.Basic
-new_frontend
 namespace Lean.Elab
 open Meta
 

src/Lean/Elab/PreDefinition/WF.lean

@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.PreDefinition.Basic
-new_frontend
 namespace Lean
 namespace Elab
 open Meta

src/Lean/Elab/Tactic/Basic.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -12,7 +13,6 @@ import Lean.Meta.Tactic.Subst
 import Lean.Elab.Util
 import Lean.Elab.Term
 import Lean.Elab.Binders
-new_frontend
 namespace Lean.Elab
 open Meta
 

src/Lean/Elab/Tactic/Binders.lean

@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Tactic.Basic
-new_frontend
 namespace Lean.Elab.Tactic
 
 private def liftTermBinderSyntax : Macro :=

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assert
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.SyntheticMVars
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta

src/Lean/Elab/Tactic/Generalize.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -7,7 +8,6 @@ import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
 import Lean.Elab.Tactic.ElabTerm
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta

src/Lean/Elab/Tactic/Induction.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -9,7 +10,6 @@ import Lean.Meta.Tactic.Induction
 import Lean.Meta.Tactic.Cases
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Generalize
-new_frontend
 
 namespace Lean.Elab.Tactic
 open Meta

src/Lean/Elab/Tactic/Injection.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,7 +6,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Injection
 import Lean.Elab.Tactic.ElabTerm
-new_frontend
 namespace Lean.Elab.Tactic
 
 -- optional (" with " >> many1 ident')

src/Lean/Elab/Tactic/Location.lean

@@ -1,9 +1,9 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-new_frontend
 namespace Lean.Elab.Tactic
 
 inductive Location

src/Lean/Elab/Tactic/Match.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,7 +7,6 @@ Authors: Leonardo de Moura
 import Lean.Elab.Match
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Induction
-new_frontend
 
 namespace Lean.Elab.Tactic
 

src/Lean/Elab/Tactic/Rewrite.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,7 +9,6 @@ import Lean.Meta.Tactic.Replace
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
-new_frontend
 namespace Lean.Elab.Tactic
 open Meta