diff --git a/tests/lean/interactive/alias.input b/tests/lean/interactive/alias.input
deleted file mode 100644
index 04f039f4e..000000000
--- a/tests/lean/interactive/alias.input
+++ /dev/null
@@ -1,15 +0,0 @@
-VISIT alias.lean
-SET
-pp.notation false
-REPLACE 1
-import data.bool
-WAIT
-FINDP 1
-tt
-REPLACE 2
-open bool
-REPLACE 3
-check tt
-WAIT
-FINDP 3
-tt
diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out
deleted file mode 100644
index 442440e2a..000000000
--- a/tests/lean/interactive/alias.input.expected.out
+++ /dev/null
@@ -1,46 +0,0 @@
--- BEGINSET
--- ENDSET
--- BEGINWAIT
--- ENDWAIT
--- BEGINFINDP
-bool.tt_bxor_tt|eq (bool.bxor bool.tt bool.tt) bool.ff
-bool.tt_bxor_ff|eq (bool.bxor bool.tt bool.ff) bool.tt
-bool.bor_tt|∀ a, eq (bool.bor a bool.tt) bool.tt
-bool.band_tt|∀ a, eq (bool.band a bool.tt) a
-bool.tt|bool
-bool.bxor_tt|∀ a, eq (bool.bxor a bool.tt) (bool.bnot a)
-bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt
-bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff
-bool.ff_bxor_tt|eq (bool.bxor bool.ff bool.tt) bool.tt
-bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B
-bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt
-tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
-bool.tt_band|∀ a, eq (bool.band bool.tt a) a
-bool.cond_tt|∀ t e, eq (bool.cond bool.tt t e) t
-bool.ff_ne_tt|eq bool.ff bool.tt → false
-bool.eq_ff_of_ne_tt|ne ?a bool.tt → eq ?a bool.ff
-bool.tt_bxor|∀ a, eq (bool.bxor bool.tt a) (bool.bnot a)
-bool.tt_bor|∀ a, eq (bool.bor bool.tt a) bool.tt
--- ENDFINDP
--- BEGINWAIT
--- ENDWAIT
--- BEGINFINDP
-tt|bool
-tt_bor|∀ a, eq (bor tt a) tt
-tt_band|∀ a, eq (band tt a) a
-tt_bxor|∀ a, eq (bxor tt a) (bnot a)
-tt_bxor_tt|eq (bxor tt tt) ff
-tt_bxor_ff|eq (bxor tt ff) tt
-bor_tt|∀ a, eq (bor a tt) tt
-band_tt|∀ a, eq (band a tt) a
-bxor_tt|∀ a, eq (bxor a tt) (bnot a)
-eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt
-eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff
-ff_bxor_tt|eq (bxor ff tt) tt
-absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B
-eq_tt_of_ne_ff|ne ?a ff → eq ?a tt
-tactic.with_attributes_tac|tactic.expr → tactic.identifier_list → tactic → tactic
-cond_tt|∀ t e, eq (cond tt t e) t
-ff_ne_tt|eq ff tt → false
-eq_ff_of_ne_tt|ne ?a tt → eq ?a ff
--- ENDFINDP
diff --git a/tests/lean/interactive/auto_comp.input b/tests/lean/interactive/auto_comp.input
deleted file mode 100644
index 489285267..000000000
--- a/tests/lean/interactive/auto_comp.input
+++ /dev/null
@@ -1,15 +0,0 @@
-VISIT auto_comp.lean
-SYNC 8
-prelude
-inductive nat  := zero : nat | succ : nat → nat
-inductive bool := ff | tt
-namespace nat
-  inductive le : nat → nat → Type.{0} := refl : Π a, le a a
-
-end nat
-
-WAIT
-FINDP 6
-rec_on
-FINDP 8
-rec_on
\ No newline at end of file
diff --git a/tests/lean/interactive/auto_comp.input.expected.out b/tests/lean/interactive/auto_comp.input.expected.out
deleted file mode 100644
index eb6105e25..000000000
--- a/tests/lean/interactive/auto_comp.input.expected.out
+++ /dev/null
@@ -1,12 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- BEGINFINDP
-le.rec_on|le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
-nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (succ a)) → ?C n
-bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
--- ENDFINDP
--- BEGINFINDP
-nat.le.rec_on|nat.le ?a ?a → (Π a, ?C a a) → ?C ?a ?a
-nat.rec_on|Π n, ?C 0 → (Π a, ?C a → ?C (nat.succ a)) → ?C n
-bool.rec_on|Π n, ?C bool.ff → ?C bool.tt → ?C n
--- ENDFINDP
diff --git a/tests/lean/interactive/num2.input b/tests/lean/interactive/num2.input
deleted file mode 100644
index b6f69685e..000000000
--- a/tests/lean/interactive/num2.input
+++ /dev/null
@@ -1,16 +0,0 @@
-VISIT num2.lean
-WAIT
-SET
-pp.notation false
-FINDP 39
-pos_num.si
-REPLACE 23
-  definition size (a : pos_num) : pos_num :=
-WAIT
-REPLACE 39
-  rec (pos pos_num.one) (λp, pos (pos_num.size p)) a
-WAIT
-FINDP 39
-pos_num.si
-FINDP 26
-pos_num.si
diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out
deleted file mode 100644
index 3e86e436d..000000000
--- a/tests/lean/interactive/num2.input.expected.out
+++ /dev/null
@@ -1,96 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- 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.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?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, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
-pos_num.one|pos_num
-pos_num.below|pos_num → Type
-pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?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.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
-pos_num.add|pos_num → pos_num → pos_num
-pos_num_has_mul|has_mul pos_num
-pos_num|Type
-pos_num_has_one|has_one pos_num
-pos_num_has_add|has_add pos_num
--- ENDFINDP
--- BEGINWAIT
--- ENDWAIT
--- BEGINWAIT
--- ENDWAIT
--- 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.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?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, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
-pos_num.one|pos_num
-pos_num.below|pos_num → Type
-pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?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.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
-pos_num.add|pos_num → pos_num → pos_num
-pos_num_has_mul|has_mul pos_num
-pos_num|Type
-pos_num_has_one|has_one pos_num
-pos_num_has_add|has_add pos_num
--- 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.binduction_on|Π n, (Π n, pos_num.ibelow n → ?C n) → ?C n
-pos_num.induction_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?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, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → (Π n, ?C n)
-pos_num.one|pos_num
-pos_num.below|pos_num → Type
-pos_num.le|pos_num → pos_num → bool
-pos_num.cases_on|Π n, ?C pos_num.one → (Π a, ?C (pos_num.bit1 a)) → (Π a, ?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.lt|pos_num → pos_num → bool
-pos_num.rec_on|Π n, ?C pos_num.one → (Π a, ?C a → ?C (pos_num.bit1 a)) → (Π a, ?C a → ?C (pos_num.bit0 a)) → ?C n
-pos_num.brec_on|Π n, (Π n, pos_num.below n → ?C n) → ?C n
-pos_num.add|pos_num → pos_num → pos_num
-pos_num_has_mul|has_mul pos_num
-pos_num|Type
-pos_num_has_one|has_one pos_num
-pos_num_has_add|has_add pos_num
--- ENDFINDP