diff -r 975d44e867be -r e911dae20737 Nominal/Term5a.thy
--- a/Nominal/Term5a.thy	Wed Mar 17 11:11:42 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-theory Term5
-imports "Parser"
-begin
-
-atom_decl name
-
-ML {* restricted_nominal := 2 *}
-
-nominal_datatype trm5 =
-  Vr5 "name"
-| Ap5 "trm5" "trm5"
-| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
-and lts =
-  Lnil
-| Lcons "name" "trm5" "lts"
-binder
-  bv5
-where
-  "bv5 Lnil = {}"
-| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
-
-lemma lets_ok:
-  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (simp add: trm5_lts_inject)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
-done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
-apply (simp only: trm5_lts_inject not_ex)
-apply (rule allI)
-apply (simp add: alpha_gen)
-apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
-done
-
-end