diff -r a7e60da429e2 -r 2b367c80c0d7 Nominal/Manual/Term5.thy
--- a/Nominal/Manual/Term5.thy	Tue Mar 23 09:13:17 2010 +0100
+++ b/Nominal/Manual/Term5.thy	Tue Mar 23 09:21:43 2010 +0100
@@ -289,56 +289,4 @@
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen]
 lemmas alpha5_DIS = alpha_dis[quot_lifted]
 
-(* why is this not in Isabelle? *)
-lemma set_sub: "{a, b} - {b} = {a} - {b}"
-by auto
-
-lemma lets_bla:
-  "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"
-apply (simp only: alpha5_INJ bv5)
-apply simp
-apply (rule allI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts)
-apply (rule impI)
-apply (rule impI)
-apply (rule impI)
-apply (simp add: set_sub)
-done
-
-lemma lets_ok:
-  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-thm alpha5_INJ
-apply (simp only: alpha5_INJ)
-apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply (simp_all add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: eqvts)
-done
-
-lemma lets_ok3:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)
-done
-
-
-lemma lets_not_ok1:
-  "x \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp add: alpha5_INJ alpha_gen)
-apply (simp add: permute_trm5_lts eqvts)
-apply (simp add: alpha5_INJ)
-done
-
-lemma lets_nok:
-  "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
-   (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
-   (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
-apply (simp add: alpha5_DIS alpha5_INJ permute_trm5_lts)
-done
-
 end