--- a/Tutorial/Minimal.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-theory Minimal
-imports "Nominal2"
-begin
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
-
-
-
-lemma alpha_test:
-  shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
-  by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
-
-end
\ No newline at end of file