diff -r 3772bb3bd7ce -r 3885dc2669f9 Nominal/Ex/Ex1rec.thy
--- a/Nominal/Ex/Ex1rec.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Ex1rec
-imports "../NewParser"
-begin
-
-declare [[STEPS = 9]]
-
-atom_decl name
-
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam"
-| Lam x::"name" t::"lam"  bind_set x in t
-| Let bp::"bp" t::"lam"   bind_set "bi bp" in bp t
-and bp =
-  Bp "name" "lam"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (Bp x t) = {atom x}"
-
-
-thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
-
-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
-thm lam_bp.supp
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp(1-2)]
-
-
-
-end
-
-
-