Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed a problem with non-existant alphas2
authorChristian Urban <urbanc@in.tum.de>
Mon, 10 May 2010 18:09:00 +0100
changeset 2101 e417be53916e
parent 2100 705dc7532ee3
child 2102 200954544cae
fixed a problem with non-existant alphas2
Nominal/Ex/ExLetRec.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/ExLetRec.thy	Mon May 10 17:57:22 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy	Mon May 10 18:09:00 2010 +0100
@@ -43,13 +43,14 @@
 
 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))"
-  by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base)
+  apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
+  done
 
 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: alphas2 fresh_star_def eqvts supp_at_base)
+  apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
   done
 
 lemma lets_ok3:
nominal2