diff -r 48c2eb84d5ce -r c0eac04ae3b4 Nominal/Ex1rec.thy
--- a/Nominal/Ex1rec.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-theory Ex1rec
-imports "Parser" "../Attic/Prove"
-begin
-
-atom_decl name
-
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaGen *}
-nominal_datatype lam' =
-  VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'"  bind x in t
-| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
-and bp' =
-  BP' "name" "lam'"
-binder
-  bi'::"bp' \<Rightarrow> atom set"
-where
-  "bi' (BP' x t) = {atom x}"
-
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
-
-end
-
-
-