diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean
deleted file mode 100644
index 543e121162..0000000000
--- a/tests/lean/run/class_bug1.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-inductive [class] category (ob : Type) (mor : ob → ob → Type) : Type
-| mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
-           (id : Π {A : ob}, mor A A),
-            (Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
-            comp h (comp g f) = comp (comp h g) f) →
-           (Π {A B : ob} {f : mor A B}, comp f id = f) →
-           (Π {A B : ob} {f : mor A B}, comp id f = f) →
-            category
-
-namespace category
-section sec_cat
-  parameter A : Type
-  inductive [class] foo
-  | mk : A → foo
-
-  parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
-  definition compose := category.rec (λ comp id assoc idr idl, comp) Cat
-  definition id := category.rec (λ comp id assoc idr idl, id) Cat
-  local infixr ∘ := compose
-  inductive is_section {A B : ob} (f : mor A B) : Type
-  | mk : ∀g : mor B A, g ∘ f = id → is_section
-end sec_cat
-end category
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
deleted file mode 100644
index 3da0632a5a..0000000000
--- a/tests/lean/run/list_elab1.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-----------------------------------------------------------------------------------------------------
---- Copyright (c) 2014 Parikshit Khanna. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Authors: Parikshit Khanna, Jeremy Avigad
-----------------------------------------------------------------------------------------------------
-
--- Theory List
--- ===========
---
--- Basic properties of Lists.
-
-open nat
-inductive List (T : Type) : Type
-| nil {} : List
-| cons : T → List → List
-
-namespace List
-theorem List_induction_on {T : Type} {P : List T → Prop} (l : List T) (Hnil : P nil)
-    (Hind : forall x : T, forall l : List T, forall H : P l, P (cons x l)) : P l :=
-List.rec Hnil Hind l
-
-definition concat {T : Type} (s t : List T) : List T :=
-List.rec t (fun x : T, fun l : List T, fun u : List T, cons x u) s
-
-attribute concat [reducible]
-theorem concat_nil {T : Type} (t : List T) : concat t nil = t :=
-List_induction_on t (eq.refl (concat nil nil))
-  (take (x : T) (l : List T) (H : concat l nil = l),
-    H ▸ (eq.refl (concat (cons x l) nil)))
-end List
diff --git a/tests/lean/run/show2.lean b/tests/lean/run/show2.lean
deleted file mode 100644
index cfa33cdc27..0000000000
--- a/tests/lean/run/show2.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-open nat
-
-example : ∀ a b : nat, a + b = b + a :=
-show ∀ a b : nat, a + b = b + a
-| 0        0        := rfl
-| 0        (succ b) := sorry -- by rewrite zero_add
-| (succ a) 0        := sorry -- by rewrite zero_add
-| (succ a) (succ b) := sorry -- by rewrite [succ_add, this]