diff --git a/tests/lean/559.lean b/tests/lean/559.lean
deleted file mode 100644
index 296d9a67dd..0000000000
--- a/tests/lean/559.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import algebra.ordered_field
-open algebra
-section sequence_c
-
-  parameter Q : Type
-  parameter lof_Q : linear_ordered_field Q
-  definition to_lof [instance] : linear_ordered_field Q := lof_Q
-  include to_lof
-
-  theorem foo (a b : Q) : a + b = b + a := add.comm a b
-
-end sequence_c
diff --git a/tests/lean/559.lean.expected.out b/tests/lean/559.lean.expected.out
deleted file mode 100644
index eb852a62a7..0000000000
--- a/tests/lean/559.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-559.lean:10:28: error: failed to synthesize placeholder
-Q : Type,
-a b : Q
-⊢ has_add Q
diff --git a/tests/lean/alias.lean b/tests/lean/alias.lean
index 2e65ab64aa..2197bf1b37 100644
--- a/tests/lean/alias.lean
+++ b/tests/lean/alias.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace N1
   constant num : Type.{1}
diff --git a/tests/lean/alias2.lean b/tests/lean/alias2.lean
index c763cad56f..896025fb36 100644
--- a/tests/lean/alias2.lean
+++ b/tests/lean/alias2.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace foo
    definition t := true
diff --git a/tests/lean/auto_include.lean b/tests/lean/auto_include.lean
deleted file mode 100644
index 77ec231fd2..0000000000
--- a/tests/lean/auto_include.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-import algebra.group
-open algebra
-
-section
-variables {A : Type} [group A]
-variables {B : Type} [group B]
-
-definition foo (a b : A) : a * b = b * a :=
-sorry
-
-definition bla (b : B) : b * 1 = b :=
-sorry
-
-print foo
-print bla
-end
-
-section
-variable {A : Type}
-variable [group A]
-variable {B : Type}
-variable [group B]
-
-definition foo2 (a b : A) : a * b = b * a :=
-sorry
-
-definition bla2 (b : B) : b * 1 = b :=
-sorry
-
-print foo2
-print bla2
-end
diff --git a/tests/lean/auto_include.lean.expected.out b/tests/lean/auto_include.lean.expected.out
deleted file mode 100644
index 26bdba0f4c..0000000000
--- a/tests/lean/auto_include.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ A _inst_1 a b, sorry
-definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ B _inst_2 b, sorry
-definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
-λ A _inst_1 a b, sorry
-definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
-λ B _inst_2 b, sorry
diff --git a/tests/lean/bad_class.lean b/tests/lean/bad_class.lean
index 574ccb9181..62e2c7f6be 100644
--- a/tests/lean/bad_class.lean
+++ b/tests/lean/bad_class.lean
@@ -1,4 +1,4 @@
-import logic
+--
 namespace foo
 definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
 attribute subsingleton [class]
diff --git a/tests/lean/bad_id.lean b/tests/lean/bad_id.lean
index 50ef61c6b9..9a7239a0b5 100644
--- a/tests/lean/bad_id.lean
+++ b/tests/lean/bad_id.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 definition x.y : nat := 10
 
diff --git a/tests/lean/bad_notation.lean b/tests/lean/bad_notation.lean
index eff773aff3..f4490679cc 100644
--- a/tests/lean/bad_notation.lean
+++ b/tests/lean/bad_notation.lean
@@ -1,4 +1,4 @@
-import logic
+--
 open nat
 
 section
diff --git a/tests/lean/by_contradiction.lean b/tests/lean/by_contradiction.lean
index 882112a081..57baac67a2 100644
--- a/tests/lean/by_contradiction.lean
+++ b/tests/lean/by_contradiction.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open tactic nat
 
 example (a b : nat) : a ≠ b → ¬ a = b :=
diff --git a/tests/lean/check.lean b/tests/lean/check.lean
index 3a4e6f7c92..05ecc7e300 100644
--- a/tests/lean/check.lean
+++ b/tests/lean/check.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 check and.intro
 check or.elim
diff --git a/tests/lean/check2.lean b/tests/lean/check2.lean
index 210449e6e3..3f2e5ca523 100644
--- a/tests/lean/check2.lean
+++ b/tests/lean/check2.lean
@@ -1,3 +1,3 @@
-import logic
+--
 
 check eq.rec_on
diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean
index ca62a559d5..2775429be1 100644
--- a/tests/lean/cls_err.lean
+++ b/tests/lean/cls_err.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 inductive H [class] (A : Type) :=
 mk : A → H A
diff --git a/tests/lean/congr_print.lean b/tests/lean/congr_print.lean
deleted file mode 100644
index 1ce78d87f6..0000000000
--- a/tests/lean/congr_print.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import data.list
-open list perm
-
-set_option pp.max_depth 10
-print perm_erase_dup_of_perm
diff --git a/tests/lean/congr_print.lean.expected.out b/tests/lean/congr_print.lean.expected.out
deleted file mode 100644
index 5ea232a9c0..0000000000
--- a/tests/lean/congr_print.lean.expected.out
+++ /dev/null
@@ -1,2 +0,0 @@
-theorem perm.perm_erase_dup_of_perm [congr] : ∀ {A : Type} [H : decidable_eq A] {l₁ l₂ : list A}, l₁ ~ l₂ → erase_dup l₁ ~ erase_dup l₂ :=
-λ A H l₁ l₂, sorry
diff --git a/tests/lean/const.lean b/tests/lean/const.lean
index 2e4bba4254..cec1eed660 100644
--- a/tests/lean/const.lean
+++ b/tests/lean/const.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 
 definition foo {A : Type} [H : inhabited A] : A :=
diff --git a/tests/lean/crash.lean b/tests/lean/crash.lean
index 1130a7fe72..782278b815 100644
--- a/tests/lean/crash.lean
+++ b/tests/lean/crash.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 section
 hypothesis P : Prop.
diff --git a/tests/lean/ctxopt.lean b/tests/lean/ctxopt.lean
index f527b73981..f805d9847b 100644
--- a/tests/lean/ctxopt.lean
+++ b/tests/lean/ctxopt.lean
@@ -1,4 +1,4 @@
-import logic
+--
 -- definition id {A : Type} (a : A) := a
 
 section
diff --git a/tests/lean/elab10.lean b/tests/lean/elab10.lean
deleted file mode 100644
index 954aeb713b..0000000000
--- a/tests/lean/elab10.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import algebra.ring
-set_option pp.notation false
-set_option pp.implicit true
-set_option pp.numerals false
-set_option pp.binder_types true
-
-check ∀ (A : Type) [has_add A] [has_zero A] [has_lt A] (a : A), a = 0 + 0 → a + a > 0
-
-constant int : Type₁
-constant int_comm_ring : comm_ring int
-attribute int_comm_ring [instance]
-
-check int → int
-
-check ((λ x, x + 1) : int → int)
-
-check λ (A : Type) (a b c d : A) (H1 : a = b) (H2 : b = c) (H3 : d = c),
-     have a = c, from eq.trans H1 H2,
-     have H3' : c = d, from eq.symm H3,
-     show a = d, from eq.trans this H3'
diff --git a/tests/lean/elab10.lean.expected.out b/tests/lean/elab10.lean.expected.out
deleted file mode 100644
index 2fd1e02840..0000000000
--- a/tests/lean/elab10.lean.expected.out
+++ /dev/null
@@ -1,14 +0,0 @@
-∀ (A : Type) [_inst_1 : has_add A] [_inst_2 : has_zero A] [_inst_3 : has_lt A] (a : A),
-  @eq A a (@add A _inst_1 (@zero A _inst_2) (@zero A _inst_2)) →
-  @gt A _inst_3 (@add A _inst_1 a a) (@zero A _inst_2) :
-  Prop
-int → int : Type
-λ (x : int),
-  @add int (@distrib.to_has_add int (@ring.to_distrib int (@comm_ring.to_ring int int_comm_ring))) x
-    (@one int (@monoid.to_has_one int (@ring.to_monoid int (@comm_ring.to_ring int int_comm_ring)))) :
-  int → int
-λ (A : Type) (a b c d : A) (H1 : @eq A a b) (H2 : @eq A b c) (H3 : @eq A d c),
-  have this : @eq A a c, from @eq.trans A a b c H1 H2,
-  have H3' : @eq A c d, from @eq.symm A d c H3,
-  show @eq A a d, from @eq.trans A a c d this H3' :
-  ∀ (A : Type) (a b c d : A), @eq A a b → @eq A b c → @eq A d c → @eq A a d
diff --git a/tests/lean/empty.lean b/tests/lean/empty.lean
index b4948f6665..115db4ea55 100644
--- a/tests/lean/empty.lean
+++ b/tests/lean/empty.lean
@@ -1,4 +1,4 @@
-import logic
+--
 open inhabited nonempty classical
 
 noncomputable definition v1 : Prop := epsilon (λ x, true)
diff --git a/tests/lean/error_loc_bug.lean b/tests/lean/error_loc_bug.lean
deleted file mode 100644
index 61b770efe5..0000000000
--- a/tests/lean/error_loc_bug.lean
+++ /dev/null
@@ -1,78 +0,0 @@
-/-
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-
-Define propositional calculus, valuation, provability, validity, prove soundness.
-
-This file is based on Floris van Doorn Coq files.
-
-Similar to soundness.lean, but defines Nc in Type.
-The idea is to be able to prove soundness using recursive equations.
--/
-import data.nat data.list
-open nat bool list decidable
-
-definition PropVar [reducible] := nat
-
-inductive PropF :=
-| Var  : PropVar → PropF
-| Bot  : PropF
-| Conj : PropF → PropF → PropF
-| Disj : PropF → PropF → PropF
-| Impl : PropF → PropF → PropF
-
-namespace PropF
-  notation `#`:max P:max := Var P
-  local notation A ∨ B   := Disj A B
-  local notation A ∧ B   := Conj A B
-  infixr `⇒`:27          := Impl
-  notation `⊥`           := Bot
-
-  definition Neg A       := A ⇒ ⊥
-  notation ~ A           := Neg A
-  definition Top         := ~⊥
-  notation `⊤`           := Top
-  definition BiImpl A B  := A ⇒ B ∧ B ⇒ A
-  infixr `⇔`:27          := BiImpl
-
-  definition valuation   := PropVar → bool
-
-  reserve infix ` ⊢ `:26
-
-  /- Provability -/
-
-  inductive Nc : list PropF → PropF → Type :=
-  infix ⊢ := Nc
-  | Nax   : ∀ Γ A,   A ∈ Γ →             Γ ⊢ A
-  | ImpI  : ∀ Γ A B, A::Γ ⊢ B →          Γ ⊢ A ⇒ B
-  | ImpE  : ∀ Γ A B, Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
-  | BotC  : ∀ Γ A,   (~A)::Γ ⊢ ⊥ →       Γ ⊢ A
-  | AndI  : ∀ Γ A B, Γ ⊢ A → Γ ⊢ B →     Γ ⊢ A ∧ B
-  | AndE₁ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ A
-  | AndE₂ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ B
-  | OrI₁  : ∀ Γ A B, Γ ⊢ A →             Γ ⊢ A ∨ B
-  | OrI₂  : ∀ Γ A B, Γ ⊢ B →             Γ ⊢ A ∨ B
-  | OrE   : ∀ Γ A B C, Γ ⊢ A ∨ B → A::Γ ⊢ C → B::Γ ⊢ C → Γ ⊢ C
-
-  infix ⊢ := Nc
-  open Nc
-
-  -- Remark ⌞t⌟ indicates we should not pattern match on t.
-  -- In the following lemma, we only need to pattern match on Γ ⊢ A,
-
-  lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
-  | Γ A       Δ (Nax Γ A Hin)          Hs := Nax _ _ (Hs A Hin)
-  | Γ (A ⇒ B) Δ (ImpI Γ A B H)         Hs := ImpI _ _ _ (weakening2 H (cons_sub_cons A Hs))
-  | Γ B       Δ (ImpE Γ A B H₁ H₂)     Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | Γ A       Δ (BotC Γ A H)           Hs := BotC _ _ (weakening2 H (cons_sub_cons (~A) Hs))
-  | Γ (A ∧ B) Δ (AndI Γ A B H₁ H₂)     Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | Γ A       Δ (AndE₁ Γ A B H)        Hs := AndE₁ _ _ _ (weakening2 H Hs)
-  | Γ B       Δ (AndE₂ Γ A B H)        Hs := AndE₂ _ _ _ (weakening2 H Hs)
-  | Γ (A ∧ B) Δ (OrI₁ Γ A B H)         Hs := OrI₁ _ _ _ (weakening2 H Hs)
-  | Γ (A ∨ B) Δ (OrI₂ Γ A B H)         Hs := OrI₂ _ _ _ (weakening2 H Hs)
-  | Γ C       Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
-       OrE _ _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ (cons_sub_cons A Hs)) (weakening2 H₃ (cons_sub_cons B Hs))
-
-end PropF
diff --git a/tests/lean/error_loc_bug.lean.expected.out b/tests/lean/error_loc_bug.lean.expected.out
deleted file mode 100644
index 8cc6c0ec20..0000000000
--- a/tests/lean/error_loc_bug.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-error_loc_bug.lean:73:17: error: type mismatch at application
-  weakening2 (OrI₁ Γ A B H)
-term
-  OrI₁ Γ A B H
-has type
-  Γ ⊢ A ∨ B
-but is expected to have type
-  Γ ⊢ A ∧ B
diff --git a/tests/lean/eta_bug.lean b/tests/lean/eta_bug.lean
index c376ac032a..7170f8841d 100644
--- a/tests/lean/eta_bug.lean
+++ b/tests/lean/eta_bug.lean
@@ -1,4 +1,4 @@
-import logic
+--
 eval λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
 -- Should not reduce to
 -- λ (A : Type) (x y : A), eq.trans
diff --git a/tests/lean/export1.lean b/tests/lean/export1.lean
deleted file mode 100644
index 78c78427ab..0000000000
--- a/tests/lean/export1.lean
+++ /dev/null
@@ -1,38 +0,0 @@
-import data.nat
-
-namespace foo
-  export nat
-  check gcd
-end foo
-
-check gcd
-
-namespace foo
-  check gcd
-end foo
-
-check gcd
-
-namespace bla
-   check gcd
-   export foo
-   check gcd
-end bla
-
-section
-  open bla
-  check gcd
-end
-
-check gcd
-
-section
-  open foo
-  check gcd
-end
-
-check gcd
-
-open bla foo nat
-print raw gcd
-check gcd
diff --git a/tests/lean/export1.lean.expected.out b/tests/lean/export1.lean.expected.out
deleted file mode 100644
index c6467d778b..0000000000
--- a/tests/lean/export1.lean.expected.out
+++ /dev/null
@@ -1,12 +0,0 @@
-gcd : ℕ → ℕ → ℕ
-export1.lean:8:6: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-export1.lean:14:6: error: unknown identifier 'gcd'
-export1.lean:17:9: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-gcd : ℕ → ℕ → ℕ
-export1.lean:27:6: error: unknown identifier 'gcd'
-gcd : ℕ → ℕ → ℕ
-export1.lean:34:6: error: unknown identifier 'gcd'
-gcd
-gcd : ℕ → ℕ → ℕ
diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean
deleted file mode 100644
index 341e856e0b..0000000000
--- a/tests/lean/have1.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import logic
-open bool tactic eq
-notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
-notation H1 ⬝ H2 := trans H1 H2
-constants a b c : bool
-axiom H1 : a = b
-axiom H2 : b = c
-check have e1 : a = b, from H1,
-      have e2 : a = c, from sorry, -- by apply trans; apply e1; apply H2,
-      have e3 : c = a, from e2⁻¹,
-      have e4 : b = a, from e1⁻¹,
-      have e5 : b = c, from e4 ⬝ e2,
-      have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
-      e3 ⬝ e2
diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out
deleted file mode 100644
index 94fd08c5ca..0000000000
--- a/tests/lean/have1.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-have e1 : a = b, from H1,
-have e2 : a = c, from sorry,
-have e3 : c = a, from e2⁻¹,
-have e4 : b = a, from e1⁻¹,
-have e5 : b = c, from e4 ⬝ e2,
-have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
-e3 ⬝ e2 :
-  c = c
diff --git a/tests/lean/ind_parser_bug.lean b/tests/lean/ind_parser_bug.lean
index 25d4634f58..f8bc803c2e 100644
--- a/tests/lean/ind_parser_bug.lean
+++ b/tests/lean/ind_parser_bug.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 inductive acc1 (A : Type) (R : A → A → Prop) (a : A) :  Prop :=
 intro : ∀ (x : A), (∀ (y : A), R y x → acc1 A R y) → acc1 A R x
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 441d6d555d..5d0a75a1c8 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,4 +1,4 @@
-import logic data.prod
+--
 set_option pp.notation false
 
 inductive C [class] (A : Type) :=
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index 58b36b4d0a..a2769c9ef3 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 constant f : num → num → num → num
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 342198cc29..92b5e081a4 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 constant f : num → num → num → num
diff --git a/tests/lean/nested1.lean b/tests/lean/nested1.lean
index dd5a486426..4303568fe7 100644
--- a/tests/lean/nested1.lean
+++ b/tests/lean/nested1.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 namespace test
diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean
index 48044d5e9c..42eb24985d 100644
--- a/tests/lean/no_confusion_type.lean
+++ b/tests/lean/no_confusion_type.lean
@@ -1,4 +1,4 @@
-import logic
+--
 open nat
 
 inductive vector (A : Type) : nat → Type :=
diff --git a/tests/lean/notation.lean b/tests/lean/notation.lean
index e9cef7b601..2611c923ca 100644
--- a/tests/lean/notation.lean
+++ b/tests/lean/notation.lean
@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 constant b : num
 check b + b + b
diff --git a/tests/lean/notation2.lean b/tests/lean/notation2.lean
index 4b7831d024..7ba4a991dd 100644
--- a/tests/lean/notation2.lean
+++ b/tests/lean/notation2.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 infixr `::` := cons
 check (1:num) :: 2 :: nil
diff --git a/tests/lean/notation3.lean b/tests/lean/notation3.lean
index 2d5be511f1..9f4789485a 100644
--- a/tests/lean/notation3.lean
+++ b/tests/lean/notation3.lean
@@ -1,4 +1,4 @@
-import data.prod data.num
+--
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `, ` (h t, cons h t) nil) `]` := l
 open prod num
 constants a b : num
diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean
index 3bc52ee454..4290f5ebcb 100644
--- a/tests/lean/notation4.lean
+++ b/tests/lean/notation4.lean
@@ -1,4 +1,4 @@
-import logic data.sigma
+--
 open sigma
 inductive List (T : Type) : Type := nil {} : List T | cons   : T → List T → List T open List notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check ∃ (A : Type₁) (x y : A), x = y
diff --git a/tests/lean/notation5.lean b/tests/lean/notation5.lean
index 59646ea799..1e49eafb61 100644
--- a/tests/lean/notation5.lean
+++ b/tests/lean/notation5.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 notation `((` := 1
 
diff --git a/tests/lean/notation6.lean b/tests/lean/notation6.lean
index a98117c8e5..07b91d5743 100644
--- a/tests/lean/notation6.lean
+++ b/tests/lean/notation6.lean
@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 notation `o` := (10:num)
 check 11
diff --git a/tests/lean/notation7.lean b/tests/lean/notation7.lean
index 9792c8c3c8..309bbde50c 100644
--- a/tests/lean/notation7.lean
+++ b/tests/lean/notation7.lean
@@ -1,4 +1,4 @@
-import logic data.num
+--
 open num
 
 constant f : num → num
diff --git a/tests/lean/num.lean b/tests/lean/num.lean
index 5c58f8b32b..f3b8460075 100644
--- a/tests/lean/num.lean
+++ b/tests/lean/num.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 
 check 10
diff --git a/tests/lean/num3.lean b/tests/lean/num3.lean
index 0d906a037e..38812beb18 100644
--- a/tests/lean/num3.lean
+++ b/tests/lean/num3.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 set_option pp.notation false
 set_option pp.implicit true
 
diff --git a/tests/lean/num4.lean b/tests/lean/num4.lean
index 954c75a73a..f10cf0fc77 100644
--- a/tests/lean/num4.lean
+++ b/tests/lean/num4.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 set_option pp.notation false
 set_option pp.implicit true
 
diff --git a/tests/lean/num5.lean b/tests/lean/num5.lean
index 6842775349..ee1d7226c2 100644
--- a/tests/lean/num5.lean
+++ b/tests/lean/num5.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 open num
 
 eval 3+(2:num)
diff --git a/tests/lean/param.lean b/tests/lean/param.lean
index 6c8ab07a25..270371fb7e 100644
--- a/tests/lean/param.lean
+++ b/tests/lean/param.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 open num
 
 definition foo1 a b c := a + b + (c:num)
diff --git a/tests/lean/parsing_only.lean b/tests/lean/parsing_only.lean
index e542e4cc68..c5b1392ac0 100644
--- a/tests/lean/parsing_only.lean
+++ b/tests/lean/parsing_only.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 constant f : num → num
 constant g : num → num
diff --git a/tests/lean/pp_algebra_num_bug.lean b/tests/lean/pp_algebra_num_bug.lean
deleted file mode 100644
index d59087ba65..0000000000
--- a/tests/lean/pp_algebra_num_bug.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import algebra.group
-open algebra
-
-variable {A : Type}
-variable [s : group A]
-variable (a : A)
-
-check 1 * 1 * a
-set_option pp.notation false
-check 1 * a
-
-variable [s2 : add_comm_group A]
-
-set_option pp.notation true
-
-check 0 + a
-
-set_option pp.notation false
-check 0 + a
diff --git a/tests/lean/pp_algebra_num_bug.lean.expected.out b/tests/lean/pp_algebra_num_bug.lean.expected.out
deleted file mode 100644
index 4f9d8d1ff8..0000000000
--- a/tests/lean/pp_algebra_num_bug.lean.expected.out
+++ /dev/null
@@ -1,4 +0,0 @@
-1 * 1 * a : A
-mul 1 a : A
-0 + a : A
-add 0 a : A
diff --git a/tests/lean/pp_all.lean b/tests/lean/pp_all.lean
index d6bb290d7d..7eabb987e1 100644
--- a/tests/lean/pp_all.lean
+++ b/tests/lean/pp_all.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 variables {a : nat}
diff --git a/tests/lean/pp_all2.lean b/tests/lean/pp_all2.lean
index e9922e7213..9f991d039d 100644
--- a/tests/lean/pp_all2.lean
+++ b/tests/lean/pp_all2.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 
 set_option pp.all       true
 set_option pp.numerals  true
diff --git a/tests/lean/pp_no_proofs.lean b/tests/lean/pp_no_proofs.lean
index 2953a64096..ad7d88004a 100644
--- a/tests/lean/pp_no_proofs.lean
+++ b/tests/lean/pp_no_proofs.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat
 
 constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0)
diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean
index 746f4d5c0b..b255910308 100644
--- a/tests/lean/protected.lean
+++ b/tests/lean/protected.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 namespace foo
   protected definition C := true
diff --git a/tests/lean/record_rec_protected.lean b/tests/lean/record_rec_protected.lean
index c6e6e2d25b..9f97ae68d6 100644
--- a/tests/lean/record_rec_protected.lean
+++ b/tests/lean/record_rec_protected.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)
diff --git a/tests/lean/reserve_bugs.lean b/tests/lean/reserve_bugs.lean
index 57fd940e9f..71ec5f59b9 100644
--- a/tests/lean/reserve_bugs.lean
+++ b/tests/lean/reserve_bugs.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 constant f : num → num
 constant g : num → num → num
diff --git a/tests/lean/rewrite1.lean b/tests/lean/rewrite1.lean
deleted file mode 100644
index f956da7d21..0000000000
--- a/tests/lean/rewrite1.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-import data.nat
-open nat tactic
-
-example (a b : nat) : a * 0 + 0 + b + 0 = b :=
-by do
- rewrite `mul_zero,
- trace_state,
- rewrite `add_zero,
- repeat $ rewrite `zero_add
-
-print "---------"
-
-example (a b : nat) (H : a + b * 0 + 0 = b) : b = a :=
-by do
- rewrite_at `mul_zero `H,
- trace_state,
- rewrite_at `add_zero `H,
- rewrite_at `add_zero `H,
- symmetry,
- assumption
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by rewrite `zero_add
-
-meta_definition rewrite_occs (th_name : name) (occs : list nat) : tactic unit :=
-do th ← mk_const th_name,
-   rewrite_core reducible tt (occurrences.pos occs) ff th,
-   try reflexivity
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by do
-   rewrite_occs `zero_add [1, 3],
-   trace_state,
-   rewrite `zero_add
-
-print "---------"
-
-example (a : nat) : (0 + a) + (0 + a) + (0 + a) = a + a + a :=
-by do
-   rewrite_occs `zero_add [2],
-   trace_state,
-   rewrite_occs `zero_add [2],
-   trace_state,
-   rewrite `zero_add
diff --git a/tests/lean/rewrite1.lean.expected.out b/tests/lean/rewrite1.lean.expected.out
deleted file mode 100644
index f9996daa5a..0000000000
--- a/tests/lean/rewrite1.lean.expected.out
+++ /dev/null
@@ -1,15 +0,0 @@
-a b : ℕ
-⊢ 0 + 0 + b + 0 = b
----------
-a b : ℕ,
-H : a + 0 + 0 = b
-⊢ b = a
----------
----------
-a : ℕ
-⊢ a + (0 + a) + a = a + a + a
----------
-a : ℕ
-⊢ 0 + a + a + (0 + a) = a + a + a
-a : ℕ
-⊢ 0 + a + a + a = a + a + a
diff --git a/tests/lean/rquote.lean b/tests/lean/rquote.lean
index 9574aa42d0..f2cca2bf06 100644
--- a/tests/lean/rquote.lean
+++ b/tests/lean/rquote.lean
@@ -1,5 +1,5 @@
-import data.nat
-
+--
+constant nat.gcd : nat → nat → nat
 namespace foo
  constant f : nat → nat
  constant g : nat → nat
diff --git a/tests/lean/sec.lean b/tests/lean/sec.lean
index ec306d76ee..599b3f0371 100644
--- a/tests/lean/sec.lean
+++ b/tests/lean/sec.lean
@@ -1,4 +1,4 @@
-import data.prod
+--
 open prod
 
 section
diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean
deleted file mode 100644
index 6ab53969ac..0000000000
--- a/tests/lean/show1.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import logic
-open bool eq tactic
-notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
-notation H1 ⬝ H2 := trans H1 H2
-constants a b c : bool
-axiom H1 : a = b
-axiom H2 : b = c
-check show a = c, from H1 ⬝ H2
-print "------------"
-check have e1 : a = b, from H1,
-      have e2 : a = c, from sorry, -- by apply eq.trans; apply e1; apply H2,
-      have e3 : c = a, from e2⁻¹,
-      have e4 : b = a, from e1⁻¹,
-      show b = c, from e1⁻¹ ⬝ e2
diff --git a/tests/lean/show1.lean.expected.out b/tests/lean/show1.lean.expected.out
deleted file mode 100644
index 052db296b0..0000000000
--- a/tests/lean/show1.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-show a = c, from H1 ⬝ H2 : a = c
-------------
-have e1 : a = b, from H1,
-have e2 : a = c, from sorry,
-have e3 : c = a, from e2⁻¹,
-have e4 : b = a, from e1⁻¹,
-show b = c, from e1⁻¹ ⬝ e2 :
-  b = c
diff --git a/tests/lean/subpp.lean b/tests/lean/subpp.lean
index 1a18cc3190..3f67d67df9 100644
--- a/tests/lean/subpp.lean
+++ b/tests/lean/subpp.lean
@@ -1,4 +1,4 @@
--- import data.subtype
+--
 open nat subtype
 
 check {x : nat \ x > 0 }
diff --git a/tests/lean/tuple.lean b/tests/lean/tuple.lean
index 6cffe335c6..b2aa631d20 100644
--- a/tests/lean/tuple.lean
+++ b/tests/lean/tuple.lean
@@ -1,4 +1,4 @@
-import data.prod
+--
 open nat prod
 
 set_option pp.universes true
diff --git a/tests/lean/unfold2.lean b/tests/lean/unfold2.lean
deleted file mode 100644
index 914d5dae38..0000000000
--- a/tests/lean/unfold2.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import data.nat
-open nat
-
-definition fact1 : nat → nat
-| 0        := 1
-| (succ a) := (succ a) * fact1 a
-
-open tactic
-
-example (a : nat) : fact1 a > 0 :=
-by do
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH],
-  trace_state, trace "-------",
-  unfold [`fact1],
-  swap,
-  unfold [`fact1],
-  trace_state,
-  mk_const `mul_pos >>= apply,
-  mk_const `nat.zero_lt_succ >>= apply,
-  assumption,
-  mk_const `zero_lt_one >>= apply
diff --git a/tests/lean/unfold2.lean.expected.out b/tests/lean/unfold2.lean.expected.out
deleted file mode 100644
index 5db86e38e2..0000000000
--- a/tests/lean/unfold2.lean.expected.out
+++ /dev/null
@@ -1,11 +0,0 @@
-⊢ fact1 0 > 0
-
-n : ℕ,
-iH : fact1 n > 0
-⊢ fact1 (succ n) > 0
--------
-n : ℕ,
-iH : fact1 n > 0
-⊢ succ n * fact1 n > 0
-
-⊢ 1 > 0
diff --git a/tests/lean/unfold3.lean b/tests/lean/unfold3.lean
deleted file mode 100644
index 01804d5063..0000000000
--- a/tests/lean/unfold3.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-import data.nat
-open nat tactic
-
-definition fib : nat → nat
-| 0        := 1
-| 1        := 1
-| (n+2)    := fib n + fib (n+1)
-
-example (a : nat) : fib a > 0 :=
-by do
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH1],
-  trace_state, trace "-------",
-  unfold [`fib],
-  trace_state, trace "-------",
-  mk_const `zero_lt_one >>= apply,
-  trace_state, trace "-------",
-  get_local `n >>= cases,
-  unfold [`fib],
-  mk_const `zero_lt_one >>= apply,
-  unfold [`fib],
-  trace_state,
-  mk_const `add_pos_of_nonneg_of_pos >>= apply,
-  mk_const `nat.zero_le >>= apply,
-  assumption
diff --git a/tests/lean/unfold3.lean.expected.out b/tests/lean/unfold3.lean.expected.out
deleted file mode 100644
index b4a5bf2442..0000000000
--- a/tests/lean/unfold3.lean.expected.out
+++ /dev/null
@@ -1,19 +0,0 @@
-⊢ fib 0 > 0
-
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-⊢ 1 > 0
-
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-n : ℕ,
-iH1 : fib n > 0
-⊢ fib (succ n) > 0
--------
-a : ℕ,
-iH1 : fib (succ a) > 0
-⊢ fib a + fib (succ a) > 0
diff --git a/tests/lean/unfold4.lean b/tests/lean/unfold4.lean
index ef58e8929f..e0d7e14e81 100644
--- a/tests/lean/unfold4.lean
+++ b/tests/lean/unfold4.lean
@@ -1,7 +1,7 @@
-import data.nat
-import init.meta.tactic
+--
+--
 open tactic
--- import init.meta.tactics
+--
 
 inductive vector (A : Type) : nat → Type :=
   | nil {} : vector A 0
diff --git a/tests/lean/unfold_crash.lean b/tests/lean/unfold_crash.lean
index 50c1c5f98c..c46021fcb3 100644
--- a/tests/lean/unfold_crash.lean
+++ b/tests/lean/unfold_crash.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open nat tactic
 
 example (a b : nat) : a = succ b → a = b + 1 :=
diff --git a/tests/lean/unfold_crash2.lean b/tests/lean/unfold_crash2.lean
index 67fe6cca53..3e9b4073f8 100644
--- a/tests/lean/unfold_crash2.lean
+++ b/tests/lean/unfold_crash2.lean
@@ -1,4 +1,4 @@
-import data.nat
+--
 open tactic
 
 inductive vector (A : Type) : nat → Type :=
diff --git a/tests/lean/unfold_fact.lean b/tests/lean/unfold_fact.lean
deleted file mode 100644
index 73ced335e7..0000000000
--- a/tests/lean/unfold_fact.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-import data.nat
-open nat
-
-definition fact1 : nat → nat
-| 0        := 1
-| (succ a) := (succ a) * fact1 a
-
-open tactic
-
-example (a : nat) : fact1 a > 0 :=
-by do
-  -- fact1 should not be unfolded since argument is not 0 or succ
-  unfold [`fact1],
-  trace_state, trace "-------",
-  get_local `a >>= λ H, induction_core semireducible H `nat.rec_on [`n, `iH],
-  -- now it should unfold
-  unfold [`fact1],
-  swap,
-  unfold [`fact1],
-  trace_state,
-  mk_const `mul_pos >>= apply,
-  mk_const `nat.zero_lt_succ >>= apply,
-  assumption,
-  mk_const `zero_lt_one >>= apply
diff --git a/tests/lean/unfold_fact.lean.expected.out b/tests/lean/unfold_fact.lean.expected.out
deleted file mode 100644
index 342f72395d..0000000000
--- a/tests/lean/unfold_fact.lean.expected.out
+++ /dev/null
@@ -1,8 +0,0 @@
-a : ℕ
-⊢ fact1 a > 0
--------
-n : ℕ,
-iH : fact1 n > 0
-⊢ succ n * fact1 n > 0
-
-⊢ 1 > 0
diff --git a/tests/lean/uni_bug1.lean b/tests/lean/uni_bug1.lean
index 4d839b544f..75d4f21c67 100644
--- a/tests/lean/uni_bug1.lean
+++ b/tests/lean/uni_bug1.lean
@@ -1,4 +1,4 @@
-import data.prod
+--
 open nat prod
 
 constant R : nat → nat → Prop
diff --git a/tests/lean/unification_hints1.lean b/tests/lean/unification_hints1.lean
index fc978cfe2a..fc375fc575 100644
--- a/tests/lean/unification_hints1.lean
+++ b/tests/lean/unification_hints1.lean
@@ -1,4 +1,4 @@
-import data.list data.nat
+--
 open list nat
 
 structure unification_constraint := {A : Type} (lhs : A) (rhs : A)
diff --git a/tests/lean/unifier_bug.lean b/tests/lean/unifier_bug.lean
index cd28be983c..68caf99b83 100644
--- a/tests/lean/unifier_bug.lean
+++ b/tests/lean/unifier_bug.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 theorem test {A B : Type} {a : A} {b : B} (H : a == b) :
            eq.rec_on (type_eq_of_heq H) a = b
diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean
index 8702fb320c..bc8d460eed 100644
--- a/tests/lean/univ.lean
+++ b/tests/lean/univ.lean
@@ -1,4 +1,4 @@
-import data.num
+--
 
 definition id2 (A : Type) (a : A) := a
 
diff --git a/tests/lean/univ_vars.lean b/tests/lean/univ_vars.lean
index a2924cb9ab..92f4c7848d 100644
--- a/tests/lean/univ_vars.lean
+++ b/tests/lean/univ_vars.lean
@@ -1,4 +1,4 @@
-import logic
+--
 set_option pp.universes true
 
 universe u
diff --git a/tests/lean/var.lean b/tests/lean/var.lean
index e8109d8c4c..99677e3310 100644
--- a/tests/lean/var.lean
+++ b/tests/lean/var.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 
 section
diff --git a/tests/lean/var2.lean b/tests/lean/var2.lean
index 6007f7c7ac..8dff452c12 100644
--- a/tests/lean/var2.lean
+++ b/tests/lean/var2.lean
@@ -1,4 +1,4 @@
-import logic
+--
 
 
 section