diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean
index 26c3d04d7..e4be7dc7c 100644
--- a/tests/lean/have1.lean
+++ b/tests/lean/have1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using bool eq_ops tactic
 
 variables a b c : bool
diff --git a/tests/lean/interactive/simple.lean b/tests/lean/interactive/simple.lean
index 7404c94b4..00b75a63b 100644
--- a/tests/lean/interactive/simple.lean
+++ b/tests/lean/interactive/simple.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace tst
 definition foo {A B : Type} (a : A) (b : B) := a
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index b329917e2..8f19a3dbc 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 
 abbreviation Type1 := Type.{1}
diff --git a/tests/lean/run/booltst.lean b/tests/lean/run/booltst.lean
index 245439c93..cd6c1d2f5 100644
--- a/tests/lean/run/booltst.lean
+++ b/tests/lean/run/booltst.lean
@@ -1,4 +1,4 @@
-import standard
+import data.bool
 using bool
 
 check ff
\ No newline at end of file
diff --git a/tests/lean/run/bug5.lean b/tests/lean/run/bug5.lean
index 6d7da80d0..d791222f1 100644
--- a/tests/lean/run/bug5.lean
+++ b/tests/lean/run/bug5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 theorem symm2 {A : Type} {a b : A} (H : a = b) : b = a
 := subst H (refl a)
diff --git a/tests/lean/run/bug6.lean b/tests/lean/run/bug6.lean
index 530d40803..9e76e438b 100644
--- a/tests/lean/run/bug6.lean
+++ b/tests/lean/run/bug6.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 section
   parameter {A : Type}
   theorem T {a b : A} (H : a = b) : b = a
diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean
index ab956f14c..43c2848cf 100644
--- a/tests/lean/run/calc.lean
+++ b/tests/lean/run/calc.lean
@@ -1,4 +1,4 @@
-import standard
+import data.num
 using num
 
 namespace foo
diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index 3487b60b9..8c01c706f 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using num prod inhabited
 
 definition H : inhabited (Prop × num × (num → num)) := _
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index e6468a682..5d4ae9feb 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using num prod nonempty inhabited
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 08e09ddc4..6a1af65c7 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using num prod inhabited
 
 section
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 3bd556d79..9ccdaaef3 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 98e1336d4..8dc09c2a0 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace algebra
   inductive mul_struct (A : Type) : Type :=
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index d72aaaf1e..9485c6e37 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using prod
 
 inductive t1 : Type :=
diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean
index c5035fc2a..cba9a37cf 100644
--- a/tests/lean/run/class7.lean
+++ b/tests/lean/run/class7.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num tactic
 
 inductive inh (A : Type) : Type :=
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index d38d9205b..d1b2809a8 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using num tactic prod
 
 inductive inh (A : Type) : Prop :=
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 4232158dd..7cd0e1ead 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace setoid
   inductive setoid : Type :=
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index 8b389ef52..b821c290f 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace setoid
   inductive setoid : Type :=
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index 93d754dfa..89f700293 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace setoid
   inductive setoid : Type :=
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index 29632118b..8e5a90ea3 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace setoid
   inductive setoid : Type :=
diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean
index ebca1e2a1..65bf94687 100644
--- a/tests/lean/run/decidable.lean
+++ b/tests/lean/run/decidable.lean
@@ -1,4 +1,4 @@
-import standard data.unit
+import logic data.unit
 using bool unit decidable
 
 variables a b c : bool
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index 66a529af7..4091252d6 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import standard struc.function
+import logic struc.function
 
 using function
 
diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean
index fc88de62c..06630a6d6 100644
--- a/tests/lean/run/elim.lean
+++ b/tests/lean/run/elim.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 variable p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean
index 90a1d2b1c..ec19115ac 100644
--- a/tests/lean/run/elim2.lean
+++ b/tests/lean/run/elim2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num tactic
 variable p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
diff --git a/tests/lean/run/full.lean b/tests/lean/run/full.lean
index 3d225eec9..38b48fc60 100644
--- a/tests/lean/run/full.lean
+++ b/tests/lean/run/full.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 namespace foo
   variable x : num.num
   check x
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index fea5029f6..6e25d91af 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,4 +1,4 @@
-import standard struc.function
+import logic struc.function
 using function num bool
 
 
diff --git a/tests/lean/run/goal.lean b/tests/lean/run/goal.lean
index 75204634b..2f5b49de1 100644
--- a/tests/lean/run/goal.lean
+++ b/tests/lean/run/goal.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem T {a b c d : Prop} (H : a) (H : b) (H : c) (H : d) : a
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index 19b8a523b..fb16ac892 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 
 section
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index 97fe37a79..ef07a783c 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 
 section
diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean
index 6a04f24ab..3cd9bcead 100644
--- a/tests/lean/run/have5.lean
+++ b/tests/lean/run/have5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 variables a b c d : Prop
 axiom Ha : a
diff --git a/tests/lean/run/id.lean b/tests/lean/run/id.lean
index 05f1ba8d2..9a44fb2f0 100644
--- a/tests/lean/run/id.lean
+++ b/tests/lean/run/id.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 definition id {A : Type} (a : A) := a
 check id id
 set_option pp.universes true
diff --git a/tests/lean/run/implicit.lean b/tests/lean/run/implicit.lean
index 1c642fb37..f9d0c10a5 100644
--- a/tests/lean/run/implicit.lean
+++ b/tests/lean/run/implicit.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 definition f {A : Type} {B : Type} (f : A → B → Prop) ⦃C : Type⦄ {R : C → C → Prop} {c : C} (H : R c c) : R c c
 := H
@@ -7,4 +7,3 @@ variable g : Prop → Prop → Prop
 variable H : true ∧ true
 
 check f g H
-
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index 15315a2a2..70cad2a88 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 inductive list (A : Type) : Type :=
diff --git a/tests/lean/run/let1.lean b/tests/lean/run/let1.lean
index 38cb8b8df..a7ba9d4f3 100644
--- a/tests/lean/run/let1.lean
+++ b/tests/lean/run/let1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 check
   let f x y := x ∧ y,
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 8cf733910..fe33dad2d 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num eq_ops
 
 inductive nat : Type :=
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 67af5214b..a57260055 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num eq_ops
 
 inductive nat : Type :=
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index 7e3c1eb1c..10f198248 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num eq_ops
 
 inductive nat : Type :=
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index d863a9f20..84c90e7cb 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num eq_ops
 
 inductive nat : Type :=
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index ee084b35d..ba9e08193 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using eq_ops
 
 inductive nat : Type :=
diff --git a/tests/lean/run/not_bug1.lean b/tests/lean/run/not_bug1.lean
index ad4995592..0e02f4ed9 100644
--- a/tests/lean/run/not_bug1.lean
+++ b/tests/lean/run/not_bug1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using bool
 
 variable list : Type.{1}
@@ -19,4 +19,3 @@ check a :: b :: nil
 check [a, b]
 check [a, b, c]
 check []
-
diff --git a/tests/lean/run/ns1.lean b/tests/lean/run/ns1.lean
index 3fabf203f..e9915d9e4 100644
--- a/tests/lean/run/ns1.lean
+++ b/tests/lean/run/ns1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace foo
 namespace boo
diff --git a/tests/lean/run/num.lean b/tests/lean/run/num.lean
index b8b2f917b..df84b567b 100644
--- a/tests/lean/run/num.lean
+++ b/tests/lean/run/num.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 check 14
 check 0
 check 3
diff --git a/tests/lean/run/ptst.lean b/tests/lean/run/ptst.lean
index 2537e4d46..1e501bb4f 100644
--- a/tests/lean/run/ptst.lean
+++ b/tests/lean/run/ptst.lean
@@ -1,4 +1,4 @@
-import standard
+import logic data.prod
 using prod
 
 -- Test tuple notation
diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean
index 5200756d1..30dfa550f 100644
--- a/tests/lean/run/root.lean
+++ b/tests/lean/run/root.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 
 variable foo : Prop
@@ -15,6 +15,3 @@ namespace N1
     print raw _root_.foo
   end N2
 end N1
-
-
-
diff --git a/tests/lean/run/section1.lean b/tests/lean/run/section1.lean
index 9b009525b..2bc6619e5 100644
--- a/tests/lean/run/section1.lean
+++ b/tests/lean/run/section1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 section
diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean
index f86d8e483..f09791b80 100644
--- a/tests/lean/run/set.lean
+++ b/tests/lean/run/set.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using bool
 
 definition set {{T : Type}} := T → bool
diff --git a/tests/lean/run/set2.lean b/tests/lean/run/set2.lean
index 0fe7af072..2bf19ce09 100644
--- a/tests/lean/run/set2.lean
+++ b/tests/lean/run/set2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using bool
 
 namespace set
diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean
index e5c024013..4e8821a1d 100644
--- a/tests/lean/run/t8.lean
+++ b/tests/lean/run/t8.lean
@@ -1,3 +1,3 @@
-import standard
+import logic
 using tactic
 print raw (by assumption)
\ No newline at end of file
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index c7d76b472..38141de19 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean
index 094e8ad74..8f9cc44b8 100644
--- a/tests/lean/run/tactic10.lean
+++ b/tests/lean/run/tactic10.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean
index 9e8291e8d..052d7eb94 100644
--- a/tests/lean/run/tactic11.lean
+++ b/tests/lean/run/tactic11.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean
index faf9ef85d..5a1128276 100644
--- a/tests/lean/run/tactic12.lean
+++ b/tests/lean/run/tactic12.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
@@ -9,8 +9,3 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
           (assume Hna, absurd Ha Hna)
           (assume Hnb, absurd Hb Hnb));
       assumption
-
-
-
-
-
diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean
index 401de949c..88b57d269 100644
--- a/tests/lean/run/tactic13.lean
+++ b/tests/lean/run/tactic13.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean
index 1cdda0811..575475cc8 100644
--- a/tests/lean/run/tactic14.lean
+++ b/tests/lean/run/tactic14.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 definition basic_tac : tactic
diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean
index 3521c1f69..da5146924 100644
--- a/tests/lean/run/tactic15.lean
+++ b/tests/lean/run/tactic15.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 variable A : Type.{1}
diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean
index 47089c880..effced0e1 100644
--- a/tests/lean/run/tactic16.lean
+++ b/tests/lean/run/tactic16.lean
@@ -1,4 +1,4 @@
-import standard data.string
+import logic data.string
 using tactic
 
 variable A : Type.{1}
diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean
index 07c2eaad7..de3360d1f 100644
--- a/tests/lean/run/tactic17.lean
+++ b/tests/lean/run/tactic17.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 variable A : Type.{1}
@@ -8,5 +8,3 @@ theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
 := by apply (@congr A A (f a) (f b));
       apply (congr_arg f);
       !assumption
-
-
diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean
index 64587d868..9a52c9211 100644
--- a/tests/lean/run/tactic18.lean
+++ b/tests/lean/run/tactic18.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 variable A : Type.{1}
@@ -9,4 +9,3 @@ theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
       apply (subst H2);
       apply refl;
       assumption
-
diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean
index 27ac93d44..87d7912a0 100644
--- a/tests/lean/run/tactic19.lean
+++ b/tests/lean/run/tactic19.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
@@ -6,4 +6,3 @@ theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c)
       apply (subst H2);
       apply refl;
       assumption
-
diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean
index a554983d0..9b378296b 100644
--- a/tests/lean/run/tactic2.lean
+++ b/tests/lean/run/tactic2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean
index 79b870a86..addbb6a28 100644
--- a/tests/lean/run/tactic20.lean
+++ b/tests/lean/run/tactic20.lean
@@ -1,12 +1,7 @@
-import standard
+import logic
 using tactic
 
 definition assump := eassumption
 
 theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := by apply trans; assump; assump
-
-
-
-
-
diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean
index 2f721b8c9..eac4b7b1d 100644
--- a/tests/lean/run/tactic21.lean
+++ b/tests/lean/run/tactic21.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 definition assump := eassumption
@@ -12,6 +12,3 @@ theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 :
 (*
 print(get_env():find("tst2"):value())
 *)
-
-
-
diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean
index a6623c176..6625af12c 100644
--- a/tests/lean/run/tactic22.lean
+++ b/tests/lean/run/tactic22.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 48dda3659..49430daf2 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num (num pos_num num_rec pos_num_rec)
 using tactic
 
diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean
index e7e60aa17..d85d7aceb 100644
--- a/tests/lean/run/tactic24.lean
+++ b/tests/lean/run/tactic24.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 definition my_tac1 := apply @refl
diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean
index 5fa7c7205..8c9ccbad6 100644
--- a/tests/lean/run/tactic25.lean
+++ b/tests/lean/run/tactic25.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 definition my_tac1 := apply @refl
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index 164abe54a..563cfa9a0 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
diff --git a/tests/lean/run/tactic27.lean b/tests/lean/run/tactic27.lean
index 20fa0cc5d..fd74f1e3b 100644
--- a/tests/lean/run/tactic27.lean
+++ b/tests/lean/run/tactic27.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 definition my_tac := repeat ([ apply @and_intro
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index 69510bd17..f5f3f1571 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean
index 0f12a64c8..d6584770b 100644
--- a/tests/lean/run/tactic29.lean
+++ b/tests/lean/run/tactic29.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 section
diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean
index b3797c6e5..781e8d773 100644
--- a/tests/lean/run/tactic3.lean
+++ b/tests/lean/run/tactic3.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
diff --git a/tests/lean/run/tactic30.lean b/tests/lean/run/tactic30.lean
index 3b745e483..ce59a9db7 100644
--- a/tests/lean/run/tactic30.lean
+++ b/tests/lean/run/tactic30.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 section
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
index 98184be23..9eb19bb9c 100644
--- a/tests/lean/run/tactic4.lean
+++ b/tests/lean/run/tactic4.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean
index 123e494f9..c25c006b0 100644
--- a/tests/lean/run/tactic5.lean
+++ b/tests/lean/run/tactic5.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean
index 6ef178c48..fa04b08c5 100644
--- a/tests/lean/run/tactic6.lean
+++ b/tests/lean/run/tactic6.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean
index 26f8042f1..afddec6e1 100644
--- a/tests/lean/run/tactic7.lean
+++ b/tests/lean/run/tactic7.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean
index 371b99bd1..812d12eae 100644
--- a/tests/lean/run/tactic8.lean
+++ b/tests/lean/run/tactic8.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean
index 3cc5dea31..c90e2f76e 100644
--- a/tests/lean/run/tactic9.lean
+++ b/tests/lean/run/tactic9.lean
@@ -1,6 +1,5 @@
-import standard
+import logic
 using tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A
 := by apply and_intro; beta; assumption; apply and_intro; !assumption
-
diff --git a/tests/lean/run/trick.lean b/tests/lean/run/trick.lean
index 20bac83ef..b7545399d 100644
--- a/tests/lean/run/trick.lean
+++ b/tests/lean/run/trick.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using num
 
 definition proj1 (x : num) (y : num) := x
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index 5d8198c7c..f67c0f183 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/unicode.lean b/tests/lean/run/unicode.lean
index 774efb2d0..9a8bc28e8 100644
--- a/tests/lean/run/unicode.lean
+++ b/tests/lean/run/unicode.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 variable N : Type
 variable α : N
diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
index e72424fee..382d17f05 100644
--- a/tests/lean/run/univ1.lean
+++ b/tests/lean/run/univ1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 namespace S1
 hypothesis I : Type
diff --git a/tests/lean/run/univ2.lean b/tests/lean/run/univ2.lean
index f752354b9..fd281567e 100644
--- a/tests/lean/run/univ2.lean
+++ b/tests/lean/run/univ2.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 
 hypothesis I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean
index 5da7d548e..36f9ef7e1 100644
--- a/tests/lean/show1.lean
+++ b/tests/lean/show1.lean
@@ -1,4 +1,4 @@
-import standard
+import logic
 using bool eq_ops tactic
 
 variables a b c : bool
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 9c17b227d..9bedcedb6 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
-import standard struc.binary
+import logic struc.binary
 using tactic num binary eq_ops
 using decidable