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.
tuned
authorChristian Urban <urbanc@in.tum.de>
Mon, 04 Jul 2011 23:55:46 +0200
changeset 2938 faf9ad681900
parent 2937 a56d422e17f6
child 2939 dc003667cd17
tuned
Nominal/Ex/Let.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/Let.thy	Mon Jul 04 23:54:05 2011 +0200
+++ b/Nominal/Ex/Let.thy	Mon Jul 04 23:55:46 2011 +0200
@@ -280,12 +280,18 @@
   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 simp_all[7]
+  prefer 2
+  apply(simp)
+  apply(simp)
+  apply(erule conjE)+
   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)
   apply (simp add: Abs_fresh_iff)
   apply (simp add: fresh_star_def)
   apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2]
   apply (simp add: bn_apply_assn2)
+  apply(erule conjE)+
+  apply(rule conjI)
   apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2)
   apply (simp add: fresh_star_def Abs_fresh_iff)
   apply assumption+
nominal2