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/Ex/LetInv.thy
changeset 2956 7e1c309bf820
parent 2950 0911cb7bf696
child 3235 5ebd327ffb96 
--- a/Nominal/Ex/LetInv.thy	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/Ex/LetInv.thy	Wed Jul 06 23:11:30 2011 +0200
@@ -238,7 +238,12 @@
   apply (auto simp add: fresh_star_def)[3]
   apply (drule_tac x="assn" in meta_spec)
   apply (simp add: Abs1_eq_iff alpha_bn_refl)
-  apply auto
+  apply auto[7]
+  prefer 2
+  apply(simp)
+  thm subst_sumC_def
+  thm THE_default_def
+  thm theI
   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)
   apply (simp add: Abs_fresh_iff)
   apply (simp add: fresh_star_def)
nominal2