diff --git a/tests/lean/acc.lean b/tests/lean/acc.lean
index aa49023d7..04be04b64 100644
--- a/tests/lean/acc.lean
+++ b/tests/lean/acc.lean
@@ -1,6 +1,6 @@
-import logic.prop
-
+namespace play
 inductive acc (A : Type) (R : A → A → Prop) :  A → Prop :=
 intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x
 
 check @acc.rec
+end play
diff --git a/tests/lean/acc_rec_bug.lean b/tests/lean/acc_rec_bug.lean
index 57dcdb980..274edc1d2 100644
--- a/tests/lean/acc_rec_bug.lean
+++ b/tests/lean/acc_rec_bug.lean
@@ -1,5 +1,4 @@
-import logic.prop
-
+namespace play
 inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
 intro : ∀x, (∀ y, R y x → acc R y) → acc R x
 
@@ -20,3 +19,4 @@ check F x₁
   (λ (y : A) (a : R y x₁),
      acc.rec (λ (x₂ : A) (ac : ∀ (y : A), R y x₂ → acc R y) (iH : Π (y : A), R y x₂ → C y), F x₂ iH)
        (ac y a))
+end play
diff --git a/tests/lean/bad_structures.lean b/tests/lean/bad_structures.lean
index 27f0755a5..e0a948933 100644
--- a/tests/lean/bad_structures.lean
+++ b/tests/lean/bad_structures.lean
@@ -1,4 +1,4 @@
-structure prod.{l} (A : Type.{l}) (B : Type.{l}) :=
+prelude namespace foo structure prod.{l} (A : Type.{l}) (B : Type.{l}) :=
 (pr1 : A) (pr2 : B)
 
 structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type :=
@@ -9,3 +9,4 @@ structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{l} :=
 
 structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
 (pr1 : A) (pr2 : B)
+end foo
diff --git a/tests/lean/bad_structures.lean.expected.out b/tests/lean/bad_structures.lean.expected.out
index bc63115e3..febcd137a 100644
--- a/tests/lean/bad_structures.lean.expected.out
+++ b/tests/lean/bad_structures.lean.expected.out
@@ -1,3 +1,3 @@
-bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
+bad_structures.lean:1:71: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
 bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
 bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment
diff --git a/tests/lean/beginend_bug.lean b/tests/lean/beginend_bug.lean
index 9c153e076..6c5b3fc69 100644
--- a/tests/lean/beginend_bug.lean
+++ b/tests/lean/beginend_bug.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic
+import logic
 open tactic
 
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean
index 9f35ec34f..9439574e2 100644
--- a/tests/lean/bug1.lean
+++ b/tests/lean/bug1.lean
@@ -1,4 +1,4 @@
-definition bool  : Type.{1}           := Type.{0}
+prelude definition bool  : Type.{1}           := Type.{0}
 definition and   (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
 infixl `∧`:25 := and
 
diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean
index e019a57b0..28a3986f8 100644
--- a/tests/lean/calc1.lean
+++ b/tests/lean/calc1.lean
@@ -1,4 +1,4 @@
-constant A : Type.{1}
+prelude constant A : Type.{1}
 definition bool : Type.{1} := Type.{0}
 constant eq : A → A → bool
 infixl `=`:50 := eq
diff --git a/tests/lean/config.lean b/tests/lean/config.lean
index a5c55627c..e900c86a6 100644
--- a/tests/lean/config.lean
+++ b/tests/lean/config.lean
@@ -1,3 +1,4 @@
 -- set_option default configuration for tests
+prelude
 set_option pp.colors  false
 set_option pp.unicode true
diff --git a/tests/lean/empty_thm.lean b/tests/lean/empty_thm.lean
index 07e0611a1..47c975a06 100644
--- a/tests/lean/empty_thm.lean
+++ b/tests/lean/empty_thm.lean
@@ -1,4 +1,4 @@
-import logic tools.tactic
+import logic
 open tactic
 
 definition simple := apply trivial
diff --git a/tests/lean/goals1.lean b/tests/lean/goals1.lean
index da193bbf1..a10ddda2b 100644
--- a/tests/lean/goals1.lean
+++ b/tests/lean/goals1.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic.eq
+prelude import logic.eq
 open tactic
 set_option pp.notation false
 
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index b5d6dbda8..0410953b2 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,4 +1,4 @@
-import logic data.prod priority
+import logic data.prod
 set_option pp.notation false
 
 inductive C [class] (A : Type) :=
diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index ced012280..08484e381 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -4,11 +4,16 @@
 false|Prop
 false.rec|Π (C : Type), false → C
 false_elim|false → ?c
+false.of_ne|?a ≠ ?a → false
 false.rec_on|Π (C : Type), false → C
 false.cases_on|Π (C : Type), false → C
+false.decidable|decidable false
 false.induction_on|∀ (C : Prop), false → C
-not_false_trivial|¬ false
 true_ne_false|¬ true = false
+eq.false_elim|?p = false → ¬ ?p
 p_ne_false|?p → ?p ≠ false
-eq_false_elim|?a = false → ¬ ?a
+decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
+not_false|¬ false
+if_false|∀ (t e : ?A), (if false then t else e) = e
+iff.false_elim|?a ↔ false → ¬ ?a
 -- ENDFINDP
diff --git a/tests/lean/interactive/in2.input.expected.out b/tests/lean/interactive/in2.input.expected.out
index 1028d6545..11093a4e5 100644
--- a/tests/lean/interactive/in2.input.expected.out
+++ b/tests/lean/interactive/in2.input.expected.out
@@ -1,10 +1,10 @@
 -- BEGINEVAL
-Type : Type
+Type₁ : Type₂
 -- ENDEVAL
 -- BEGINSET
 -- ENDSET
 -- BEGINEVAL
-Type.{1} : Type.{2}
+Type₁ : Type₂
 -- ENDEVAL
 -- BEGINWAIT
 -- ENDWAIT
diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out
index 8793f98f0..e4cbfc453 100644
--- a/tests/lean/interactive/num2.input.expected.out
+++ b/tests/lean/interactive/num2.input.expected.out
@@ -3,16 +3,26 @@
 -- BEGINSET
 -- ENDSET
 -- BEGINFINDP
+pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
+pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
+pos_num.ibelow|pos_num → Prop
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.below|pos_num → Type
 pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.pred|pos_num → pos_num
+pos_num.mul|pos_num → pos_num → pos_num
+pos_num.no_confusion_type|Type → pos_num → pos_num → Type
 pos_num.num_bits|pos_num → pos_num
+pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
 -- BEGINWAIT
@@ -23,25 +33,43 @@ pos_num|Type
 pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
+pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
+pos_num.ibelow|pos_num → Prop
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.below|pos_num → Type
 pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.pred|pos_num → pos_num
+pos_num.mul|pos_num → pos_num → pos_num
+pos_num.no_confusion_type|Type → pos_num → pos_num → Type
+pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
 -- BEGINFINDP
 pos_num.size|pos_num → pos_num
 pos_num.bit0|pos_num → pos_num
 pos_num.is_inhabited|inhabited pos_num
+pos_num.is_one|pos_num → bool
 pos_num.inc|pos_num → pos_num
+pos_num.ibelow|pos_num → Prop
 pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.succ|pos_num → pos_num
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.below|pos_num → Type
 pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
+pos_num.pred|pos_num → pos_num
+pos_num.mul|pos_num → pos_num → pos_num
+pos_num.no_confusion_type|Type → pos_num → pos_num → Type
+pos_num.no_confusion|eq ?v1 ?v2 → pos_num.no_confusion_type ?P ?v1 ?v2
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
+pos_num.add|pos_num → pos_num → pos_num
 pos_num|Type
 -- ENDFINDP
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index 93b717bf3..5741efe45 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -1,4 +1,4 @@
--- Correct version
+prelude -- Correct version
 check let bool                      := Type.{0},
           and  (p q : bool)         := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25             := and,
diff --git a/tests/lean/num2.lean b/tests/lean/num2.lean
index 2516627d7..4a2e9a85b 100644
--- a/tests/lean/num2.lean
+++ b/tests/lean/num2.lean
@@ -1,4 +1,4 @@
-set_option pp.notation false
+prelude set_option pp.notation false
 definition Prop := Type.{0}
 constant eq {A : Type} : A → A → Prop
 infixl `=`:50 := eq
diff --git a/tests/lean/omit.lean b/tests/lean/omit.lean
index 5032c601f..db426fa19 100644
--- a/tests/lean/omit.lean
+++ b/tests/lean/omit.lean
@@ -1,4 +1,4 @@
-section
+prelude section
   variable A : Type
   variable a : A
   variable c : A
diff --git a/tests/lean/pp.lean b/tests/lean/pp.lean
index 500b9d49d..144942e54 100644
--- a/tests/lean/pp.lean
+++ b/tests/lean/pp.lean
@@ -1,4 +1,4 @@
-check λ {A : Type.{1}} (B : Type.{1}) (a : A) (b : B), a
+prelude check λ {A : Type.{1}} (B : Type.{1}) (a : A) (b : B), a
 check λ {A : Type.{1}} {B : Type.{1}} (a : A) (b : B), a
 check λ (A : Type.{1}) {B : Type.{1}} (a : A) (b : B), a
 check λ (A : Type.{1}) (B : Type.{1}) (a : A) (b : B), a
diff --git a/tests/lean/prodtst.lean b/tests/lean/prodtst.lean
index 2da0c56af..7f9f0b4d3 100644
--- a/tests/lean/prodtst.lean
+++ b/tests/lean/prodtst.lean
@@ -1,7 +1,7 @@
-import type
+--
 
-inductive prod (A B : Type₊) :=
-mk : A → B → prod A B
+inductive prod2 (A B : Type₊) :=
+mk : A → B → prod2 A B
 
 set_option pp.universes true
-check @prod
+check @prod2
diff --git a/tests/lean/prodtst.lean.expected.out b/tests/lean/prodtst.lean.expected.out
index c5091d6e8..47893064a 100644
--- a/tests/lean/prodtst.lean.expected.out
+++ b/tests/lean/prodtst.lean.expected.out
@@ -1 +1 @@
-prod.{l_1 l_2} : Type.{l_1+1} → Type.{l_2+1} → Type.{max (l_1+1) (l_2+1)}
+prod2.{l_1 l_2} : Type.{l_1+1} → Type.{l_2+1} → Type.{max (l_1+1) (l_2+1)}
diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean
index 5f9b4cc23..f54dfcb7d 100644
--- a/tests/lean/run/basic.lean
+++ b/tests/lean/run/basic.lean
@@ -1,3 +1,4 @@
+prelude
 constant A.{l1 l2} : Type.{l1} → Type.{l2}
 check A
 definition tst.{l} (A : Type) (B : Type) (C : Type.{l}) : Type := A → B → C
diff --git a/tests/lean/run/beginend.lean b/tests/lean/run/beginend.lean
index e9ec1c932..01f1d15d5 100644
--- a/tests/lean/run/beginend.lean
+++ b/tests/lean/run/beginend.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic.eq
+import logic.eq
 open tactic
 
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
diff --git a/tests/lean/run/beginend2.lean b/tests/lean/run/beginend2.lean
index 87cda77bc..502dd2be4 100644
--- a/tests/lean/run/beginend2.lean
+++ b/tests/lean/run/beginend2.lean
@@ -1,4 +1,4 @@
-import hott.path tools.tactic
+import hott.path
 
 open path tactic
 open path (rec_on)
diff --git a/tests/lean/run/beginend3.lean b/tests/lean/run/beginend3.lean
index 01335cd5c..184857aae 100644
--- a/tests/lean/run/beginend3.lean
+++ b/tests/lean/run/beginend3.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic
+import logic
 open tactic
 
 theorem foo (A : Type) (a b c : A) : a = b → b = c → a = c ∧ c = a :=
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index d2b918736..618b874c9 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -1,3 +1,4 @@
+prelude
 import logic
 namespace experiment
 inductive nat : Type :=
@@ -22,10 +23,10 @@ definition is_zero (x : nat)
 := nat.rec true (λ n r, false) x
 
 theorem is_zero_zero : is_zero zero
-:= eq_true_elim (refl _)
+:= eq.true_elim (refl _)
 
 theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
-:= eq_false_elim (refl _)
+:= eq.false_elim (refl _)
 
 theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
 := nat.rec
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index 52151aa59..08c753953 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -1,6 +1,6 @@
 import data.num
 
-
+namespace play
 constants int nat real : Type.{1}
 constant nat_add  : nat → nat → nat
 constant int_add  : int → int → int
@@ -53,3 +53,4 @@ definition id (A : Type) (a : A) := a
 notation A `=` B `:` C := @eq C A B
 check nat_to_int n + nat_to_int m = (n + m) : int
 end foo
+end play
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
index 7c5596b80..0c6e5b094 100644
--- a/tests/lean/run/coe1.lean
+++ b/tests/lean/run/coe1.lean
@@ -1,3 +1,5 @@
+prelude
+
 constant A : Type.{1}
 constant B : Type.{1}
 constant f : A → B
diff --git a/tests/lean/run/coe6.lean b/tests/lean/run/coe6.lean
index 66fa38f99..1247197ce 100644
--- a/tests/lean/run/coe6.lean
+++ b/tests/lean/run/coe6.lean
@@ -1,6 +1,6 @@
 import data.unit
 open unit
-
+namespace play
 constant int : Type.{1}
 constant nat : Type.{1}
 constant izero : int
@@ -13,3 +13,4 @@ definition g [coercion] (a : unit) : nat := nzero
 set_option pp.coercions true
 check isucc star
 check nsucc star
+end play
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index ce4037d45..50ce6df7c 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.connectives algebra.function
+import algebra.function
 open function
 
 namespace congr
diff --git a/tests/lean/run/ctx.lean b/tests/lean/run/ctx.lean
index ce2499270..4475e0e72 100644
--- a/tests/lean/run/ctx.lean
+++ b/tests/lean/run/ctx.lean
@@ -1,4 +1,4 @@
-import data.nat logic.inhabited
+import data.nat
 open nat inhabited
 
 constant N : Type.{1}
diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean
index 5ef03ae68..315208880 100644
--- a/tests/lean/run/div_wf.lean
+++ b/tests/lean/run/div_wf.lean
@@ -1,4 +1,4 @@
-import data.nat data.prod logic.wf_k
+import data.nat data.prod
 open nat well_founded decidable prod eq.ops
 
 -- Auxiliary lemma used to justify recursive call
diff --git a/tests/lean/run/e1.lean b/tests/lean/run/e1.lean
index 889a2d8d1..fffe74f7e 100644
--- a/tests/lean/run/e1.lean
+++ b/tests/lean/run/e1.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constant eq : forall {A : Type}, A → A → Prop
 constant N : Type.{1}
diff --git a/tests/lean/run/e10.lean b/tests/lean/run/e10.lean
index ef62ec521..900cf9755 100644
--- a/tests/lean/run/e10.lean
+++ b/tests/lean/run/e10.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index 3e12687f6..f04676ed7 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index 0d3bb20b8..dc6482ddb 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e13.lean b/tests/lean/run/e13.lean
index 492208db0..ff04cea7d 100644
--- a/tests/lean/run/e13.lean
+++ b/tests/lean/run/e13.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index a9aae9ac9..24a83e092 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean
index 2ec9eec2b..3ef931c2f 100644
--- a/tests/lean/run/e15.lean
+++ b/tests/lean/run/e15.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean
index 9cc1134d7..2df9ba0c0 100644
--- a/tests/lean/run/e16.lean
+++ b/tests/lean/run/e16.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean
index 7835b23db..7690417fd 100644
--- a/tests/lean/run/e17.lean
+++ b/tests/lean/run/e17.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
index 82174ed3d..ee92b4d63 100644
--- a/tests/lean/run/e18.lean
+++ b/tests/lean/run/e18.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/e2.lean b/tests/lean/run/e2.lean
index 0d0f059fc..d1075ffb8 100644
--- a/tests/lean/run/e2.lean
+++ b/tests/lean/run/e2.lean
@@ -1,2 +1,3 @@
+prelude
 definition Prop := Type.{0}
 check Prop
diff --git a/tests/lean/run/e3.lean b/tests/lean/run/e3.lean
index 9c1b11e03..e22305d4a 100644
--- a/tests/lean/run/e3.lean
+++ b/tests/lean/run/e3.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop := Type.{0}
 
 definition false := ∀x : Prop, x
diff --git a/tests/lean/run/e4.lean b/tests/lean/run/e4.lean
index 6a0cff2a7..a750c6089 100644
--- a/tests/lean/run/e4.lean
+++ b/tests/lean/run/e4.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop := Type.{0}
 
 definition false : Prop := ∀x : Prop, x
diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean
index 32b97e4b6..ed2c94a3f 100644
--- a/tests/lean/run/e5.lean
+++ b/tests/lean/run/e5.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop := Type.{0}
 
 definition false : Prop := ∀x : Prop, x
diff --git a/tests/lean/run/e6.lean b/tests/lean/run/e6.lean
index 5b61f4b65..40805acb7 100644
--- a/tests/lean/run/e6.lean
+++ b/tests/lean/run/e6.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e7.lean b/tests/lean/run/e7.lean
index 13310fd8c..1aa2c6e8a 100644
--- a/tests/lean/run/e7.lean
+++ b/tests/lean/run/e7.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index 73f1e2382..ff2096575 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
index 797227b78..234758e48 100644
--- a/tests/lean/run/e9.lean
+++ b/tests/lean/run/e9.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`:65
 
 namespace nat
diff --git a/tests/lean/run/fibrant_class1.lean b/tests/lean/run/fibrant_class1.lean
index 270824c1c..f2af1bceb 100644
--- a/tests/lean/run/fibrant_class1.lean
+++ b/tests/lean/run/fibrant_class1.lean
@@ -1,5 +1,3 @@
-import general_notation type
-
 inductive fibrant [class] (T : Type) : Type :=
 fibrant_mk : fibrant T
 
diff --git a/tests/lean/run/fibrant_class2.lean b/tests/lean/run/fibrant_class2.lean
index c07ad766d..c1a07a549 100644
--- a/tests/lean/run/fibrant_class2.lean
+++ b/tests/lean/run/fibrant_class2.lean
@@ -1,5 +1,3 @@
-import general_notation
-
 inductive fibrant [class] (T : Type) : Type :=
 fibrant_mk : fibrant T
 
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index 3a01e9e49..7cf56a966 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -1,4 +1,4 @@
-import data.nat.basic data.sum data.sigma logic.wf data.bool
+import data.nat.basic data.sum data.sigma data.bool
 open nat sigma
 
 inductive tree (A : Type) : Type :=
diff --git a/tests/lean/run/gcd.lean b/tests/lean/run/gcd.lean
index f81fc8eeb..917626a10 100644
--- a/tests/lean/run/gcd.lean
+++ b/tests/lean/run/gcd.lean
@@ -1,4 +1,4 @@
-import data.nat data.prod logic.wf_k
+import data.nat data.prod
 open nat well_founded decidable prod eq.ops
 
 namespace playground
diff --git a/tests/lean/run/get_tac1.lean b/tests/lean/run/get_tac1.lean
index 66f0cdc59..f90219e21 100644
--- a/tests/lean/run/get_tac1.lean
+++ b/tests/lean/run/get_tac1.lean
@@ -1,4 +1,4 @@
-import hott.path tools.tactic
+import hott.path
 open path
 
 definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p :=
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index b48e0da12..ada7477fd 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -7,7 +7,7 @@
 
 -- Various structures with 1, *, inv, including groups.
 
-import logic.eq logic.connectives
+import logic.eq
 import data.unit data.sigma data.prod
 import algebra.function algebra.binary
 
diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean
index 9f72786ed..f1d2cfbb6 100644
--- a/tests/lean/run/group4.lean
+++ b/tests/lean/run/group4.lean
@@ -7,7 +7,7 @@
 
 -- Various structures with 1, *, inv, including groups.
 
-import logic.eq logic.connectives
+import logic.eq
 import data.unit data.sigma data.prod
 import algebra.function algebra.binary
 
diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean
index 283a79191..e087c88f0 100644
--- a/tests/lean/run/group5.lean
+++ b/tests/lean/run/group5.lean
@@ -7,7 +7,7 @@
 
 -- Various structures with 1, *, inv, including groups.
 
-import logic.eq logic.connectives
+import logic.eq
 import data.unit data.sigma data.prod
 import algebra.function algebra.binary
 
diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean
index be42f602c..9fd2e17d1 100644
--- a/tests/lean/run/have1.lean
+++ b/tests/lean/run/have1.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constants a b c : Prop
 axiom Ha : a
diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean
index 1f55029bf..bc40d4bc2 100644
--- a/tests/lean/run/have2.lean
+++ b/tests/lean/run/have2.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constants a b c : Prop
 axiom Ha : a
diff --git a/tests/lean/run/have3.lean b/tests/lean/run/have3.lean
index 5e0b6a95d..20c9adcf6 100644
--- a/tests/lean/run/have3.lean
+++ b/tests/lean/run/have3.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constants a b c : Prop
 axiom Ha : a
diff --git a/tests/lean/run/have4.lean b/tests/lean/run/have4.lean
index 1c23eff0b..754df0713 100644
--- a/tests/lean/run/have4.lean
+++ b/tests/lean/run/have4.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constants a b c : Prop
 axiom Ha : a
diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean
index ea3ca93dc..b98b07533 100644
--- a/tests/lean/run/have6.lean
+++ b/tests/lean/run/have6.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constant and : Prop → Prop → Prop
 infixl `∧`:25 := and
diff --git a/tests/lean/run/impbug1.lean b/tests/lean/run/impbug1.lean
index 5a2789f8c..0f89d8175 100644
--- a/tests/lean/run/impbug1.lean
+++ b/tests/lean/run/impbug1.lean
@@ -1,3 +1,4 @@
+prelude
 -- category
 
 definition Prop := Type.{0}
diff --git a/tests/lean/run/impbug2.lean b/tests/lean/run/impbug2.lean
index 66f2dccfb..033d59e05 100644
--- a/tests/lean/run/impbug2.lean
+++ b/tests/lean/run/impbug2.lean
@@ -1,3 +1,4 @@
+prelude
 -- category
 
 definition Prop := Type.{0}
diff --git a/tests/lean/run/impbug3.lean b/tests/lean/run/impbug3.lean
index 5c9eb720a..34f18659d 100644
--- a/tests/lean/run/impbug3.lean
+++ b/tests/lean/run/impbug3.lean
@@ -1,3 +1,4 @@
+prelude
 -- category
 
 definition Prop := Type.{0}
diff --git a/tests/lean/run/impbug4.lean b/tests/lean/run/impbug4.lean
index a4fcd6334..22e237194 100644
--- a/tests/lean/run/impbug4.lean
+++ b/tests/lean/run/impbug4.lean
@@ -1,3 +1,4 @@
+prelude
 -- category
 
 definition Prop := Type.{0}
diff --git a/tests/lean/run/ind0.lean b/tests/lean/run/ind0.lean
index cc56f124d..40ac4b304 100644
--- a/tests/lean/run/ind0.lean
+++ b/tests/lean/run/ind0.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean
index d9a8dbcc9..765fbb0ab 100644
--- a/tests/lean/run/ind2.lean
+++ b/tests/lean/run/ind2.lean
@@ -1,3 +1,4 @@
+prelude
 inductive nat : Type :=
 zero : nat,
 succ : nat → nat
diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean
index 7aabee10e..80bd169e8 100644
--- a/tests/lean/run/ind5.lean
+++ b/tests/lean/run/ind5.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 
 inductive or (A B : Prop) : Prop :=
diff --git a/tests/lean/run/indimp.lean b/tests/lean/run/indimp.lean
index 3e124076c..652ed04ae 100644
--- a/tests/lean/run/indimp.lean
+++ b/tests/lean/run/indimp.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop := Type.{0}
 
 inductive nat :=
diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean
index 623143133..e8b9745d4 100644
--- a/tests/lean/run/induniv.lean
+++ b/tests/lean/run/induniv.lean
@@ -1,3 +1,4 @@
+prelude
 inductive list (A : Type) : Type :=
 nil {} : list A,
 cons   : A → list A → list A
diff --git a/tests/lean/run/intros.lean b/tests/lean/run/intros.lean
index 863ae57cf..ccd15ba53 100644
--- a/tests/lean/run/intros.lean
+++ b/tests/lean/run/intros.lean
@@ -1,4 +1,4 @@
-import logic tools.tactic
+import logic
 open tactic
 
 theorem tst1 (a b : Prop) : a → b → b :=
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index debdee21e..3b69f4f19 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -11,7 +11,7 @@ definition is_nil {A : Type} (l : list A) : Prop
 := list.rec true (fun h t r, false) l
 
 theorem is_nil_nil (A : Type) : is_nil (@nil A)
-:= eq_true_elim (refl true)
+:= eq.true_elim (refl true)
 
 theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil
 := not_intro (assume H : cons a l = nil,
diff --git a/tests/lean/run/issue332.lean b/tests/lean/run/issue332.lean
index bcf5114af..693102e2e 100644
--- a/tests/lean/run/issue332.lean
+++ b/tests/lean/run/issue332.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic.eq
+import logic.eq
 variable {a : Type}
 
 definition foo {A : Type} : A → A :=
diff --git a/tests/lean/run/n3.lean b/tests/lean/run/n3.lean
index 576d1dbd1..f79b3b32c 100644
--- a/tests/lean/run/n3.lean
+++ b/tests/lean/run/n3.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 constant N : Type.{1}
 constant and : Prop → Prop → Prop
diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean
index c02dbf6a3..3ed24fafa 100644
--- a/tests/lean/run/n4.lean
+++ b/tests/lean/run/n4.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 context
   variable N : Type.{1}
diff --git a/tests/lean/run/n5.lean b/tests/lean/run/n5.lean
index cc17a3bb7..317c36c40 100644
--- a/tests/lean/run/n5.lean
+++ b/tests/lean/run/n5.lean
@@ -1,3 +1,4 @@
+prelude
 constant N : Type.{1}
 constant f : N → N → N → N
 constant g : N → N → N
diff --git a/tests/lean/run/ns.lean b/tests/lean/run/ns.lean
index a1448a398..c5edac337 100644
--- a/tests/lean/run/ns.lean
+++ b/tests/lean/run/ns.lean
@@ -1,3 +1,4 @@
+prelude
 constant nat : Type.{1}
 constant f : nat → nat
 
diff --git a/tests/lean/run/proj.lean b/tests/lean/run/proj.lean
index 724bdc01e..a21d773b0 100644
--- a/tests/lean/run/proj.lean
+++ b/tests/lean/run/proj.lean
@@ -1,18 +1,18 @@
-import logic
+import logic.eq
 
-inductive sigma {A : Type} (B : A → Type) :=
-mk : Π (a : A), B a → sigma B
+inductive sigma2 {A : Type} (B : A → Type) :=
+mk : Π (a : A), B a → sigma2 B
 
-#projections sigma :: proj1 proj2
+#projections sigma2 :: proj1 proj2
 
-check sigma.proj1
-check sigma.proj2
+check sigma2.proj1
+check sigma2.proj2
 
 variables {A : Type} {B : A → Type}
 variables (a : A) (b : B a)
 
-theorem tst1 : sigma.proj1 (sigma.mk a b) = a :=
+theorem tst1 : sigma2.proj1 (sigma2.mk a b) = a :=
 rfl
 
-theorem tst2 : sigma.proj2 (sigma.mk a b) = b :=
+theorem tst2 : sigma2.proj2 (sigma2.mk a b) = b :=
 rfl
diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean
index c9d5834d3..1c27b8cd0 100644
--- a/tests/lean/run/rename_tac.lean
+++ b/tests/lean/run/rename_tac.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic
+import logic
 open tactic
 
 theorem foo1 (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean
index 234517ac3..0745db264 100644
--- a/tests/lean/run/sigma_no_confusion.lean
+++ b/tests/lean/run/sigma_no_confusion.lean
@@ -1,4 +1,4 @@
-import data.sigma tools.tactic
+import data.sigma
 
 namespace sigma
   namespace manual
diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean
index cf0b9e0cc..e2ae78513 100644
--- a/tests/lean/run/simple.lean
+++ b/tests/lean/run/simple.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 context
   parameter A : Type
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index bccb6d5ca..9b6be639e 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -1,9 +1,8 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-import logic.prop logic.inhabited logic.decidable
 open inhabited decidable
-
+namespace play
 -- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
 inl : A → sum A B,
@@ -59,3 +58,4 @@ rec_on s1
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
 end sum
+end play
diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean
index 9d2f3d674..8e8b6275e 100644
--- a/tests/lean/run/t1.lean
+++ b/tests/lean/run/t1.lean
@@ -1,3 +1,4 @@
+prelude
 definition Prop : Type.{1} := Type.{0}
 print raw ((Prop))
 print raw Prop
diff --git a/tests/lean/run/t3.lean b/tests/lean/run/t3.lean
index ff469a268..cec25fd9d 100644
--- a/tests/lean/run/t3.lean
+++ b/tests/lean/run/t3.lean
@@ -1,3 +1,4 @@
+prelude
 constant int : Type.{1}
 constant nat : Type.{1}
 namespace int
diff --git a/tests/lean/run/t6.lean b/tests/lean/run/t6.lean
index e8e3bff00..07dc09eed 100644
--- a/tests/lean/run/t6.lean
+++ b/tests/lean/run/t6.lean
@@ -1,3 +1,4 @@
+prelude
 precedence `+`  : 65
 precedence `++` : 100
 constant N : Type.{1}
diff --git a/tests/lean/run/t9.lean b/tests/lean/run/t9.lean
index da4bcc5c0..5d0b77409 100644
--- a/tests/lean/run/t9.lean
+++ b/tests/lean/run/t9.lean
@@ -1,3 +1,4 @@
+prelude
 definition bool : Type.{1} := Type.{0}
 definition and (p q : bool) : bool
 := ∀ c : bool, (p → q → c) →  c
diff --git a/tests/lean/run/tac1.lean b/tests/lean/run/tac1.lean
index 58e5d0a0a..be4747664 100644
--- a/tests/lean/run/tac1.lean
+++ b/tests/lean/run/tac1.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic
+import logic
 open tactic
 
 definition mytac := apply @and.intro; apply @eq.refl
diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean
index 1657ee492..ccff603e3 100644
--- a/tests/lean/run/uuu.lean
+++ b/tests/lean/run/uuu.lean
@@ -1,3 +1,4 @@
+prelude
 -- Porting Vladimir's file to Lean
 notation `assume` binders `,` r:(scoped f, f) := r
 notation `take`   binders `,` r:(scoped f, f) := r
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 9f276d2d6..f71fb7d85 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -2,11 +2,6 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
-import general_notation
-
-notation `assume` binders `,` r:(scoped f, f) := r
-notation `take`   binders `,` r:(scoped f, f) := r
-
 definition id {A : Type} (a : A) := a
 definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
 infixr ∘ := compose
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index ad2a5f32b..747537c33 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,2 +1,10 @@
+decidable : Prop → Type₁
+inhabited : Type → Type
+nonempty : Type → Prop
 point : Type → Type → Type
+well_founded : Π {A : Type}, (A → A → Prop) → Prop
+decidable : Prop → Type₁
+inhabited : Type → Type
+nonempty : Type → Prop
 point : Type → Type → Type
+well_founded : Π {A : Type}, (A → A → Prop) → Prop
diff --git a/tests/lean/t10.lean b/tests/lean/t10.lean
index 8943c5260..14021dc72 100644
--- a/tests/lean/t10.lean
+++ b/tests/lean/t10.lean
@@ -1,4 +1,4 @@
-constant N : Type.{1}
+prelude constant N : Type.{1}
 definition B : Type.{1} := Type.{0}
 constant ite : B → N → N → N
 constant and : B → B → B
diff --git a/tests/lean/t11.lean b/tests/lean/t11.lean
index a5af8c297..104807a34 100644
--- a/tests/lean/t11.lean
+++ b/tests/lean/t11.lean
@@ -1,4 +1,4 @@
-constant A    : Type.{1}
+prelude constant A    : Type.{1}
 definition bool : Type.{1} := Type.{0}
 constant Exists (P : A → bool) : bool
 notation `exists` binders `,` b:(scoped b, Exists b) := b
diff --git a/tests/lean/t12.lean b/tests/lean/t12.lean
index 9b9f2afcf..f79c62142 100644
--- a/tests/lean/t12.lean
+++ b/tests/lean/t12.lean
@@ -1,4 +1,4 @@
-precedence `+` : 65
+prelude precedence `+` : 65
 precedence `*` : 75
 constant N : Type.{1}
 check λ (f : N -> N -> N) (g : N → N → N) (infix + := f) (infix * := g) (x y : N), x+x*y
diff --git a/tests/lean/t13.lean b/tests/lean/t13.lean
index cdf9bdb24..cef8024b6 100644
--- a/tests/lean/t13.lean
+++ b/tests/lean/t13.lean
@@ -1,4 +1,4 @@
-constant A : Type.{1}
+prelude constant A : Type.{1}
 constant f : A → A → A
 constant g : A → A → A
 precedence `+` : 65
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index 7850c5a2d..13e3b6391 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -1,4 +1,4 @@
-namespace foo
+prelude namespace foo
   constant A : Type.{1}
   constant a : A
   constant x : A
diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean
index f4e752828..12ebf8ed6 100644
--- a/tests/lean/t4.lean
+++ b/tests/lean/t4.lean
@@ -1,4 +1,4 @@
-definition Prop : Type.{1} := Type.{0}
+prelude definition Prop : Type.{1} := Type.{0}
 constant N : Type.{1}
 check N
 constant a : N
diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean
index 7460f3130..12e353779 100644
--- a/tests/lean/t6.lean
+++ b/tests/lean/t6.lean
@@ -1,4 +1,4 @@
-definition Prop : Type.{1} := Type.{0}
+prelude definition Prop : Type.{1} := Type.{0}
 section
   variable    {A : Type}  -- Mark A as implicit parameter
   variable    R : A → A → Prop
diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean
index 3eb8ebc18..7e25aae2a 100644
--- a/tests/lean/t7.lean
+++ b/tests/lean/t7.lean
@@ -1,4 +1,4 @@
-definition Prop : Type.{1} := Type.{0}
+prelude definition Prop : Type.{1} := Type.{0}
 constant and : Prop → Prop → Prop
 context
   parameter {A : Type}  -- Mark A as implicit parameter
diff --git a/tests/lean/t9.lean b/tests/lean/t9.lean
index 4c0afbe75..dbd15cd4e 100644
--- a/tests/lean/t9.lean
+++ b/tests/lean/t9.lean
@@ -1,4 +1,4 @@
-precedence `+` : 65
+prelude precedence `+` : 65
 precedence `*` : 75
 precedence `=` : 50
 precedence `≃` : 50
diff --git a/tests/lean/tactic_var_bug.lean b/tests/lean/tactic_var_bug.lean
index 34a7d982c..cb2b7f2b3 100644
--- a/tests/lean/tactic_var_bug.lean
+++ b/tests/lean/tactic_var_bug.lean
@@ -1,4 +1,4 @@
-import tools.tactic logic.prop
+--
 
 variable p : Prop
 definition foo (q : Prop) : q → true :=