Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/ExLetRec.thy
changeset 1674 7eb95f86f87f
parent 1604 5ab97f43ec24
child 1685 721d92623c9d 
--- a/Nominal/ExLetRec.thy	Sat Mar 27 08:42:07 2010 +0100
+++ b/Nominal/ExLetRec.thy	Sat Mar 27 09:15:09 2010 +0100
@@ -35,14 +35,13 @@
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub)
-  done
+  by (simp add: trm_lts.eq_iff alphas2 set_sub)
 
 lemma lets_ok:
   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alpha_gen2 fresh_star_def eqvts)
+  apply (simp_all add: alphas2 fresh_star_def eqvts)
   done
 
 lemma lets_ok3:
nominal2