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/CPS/Lt.thy
changeset 3231 188826f1ccdb
parent 3197 25d11b449e92
child 3235 5ebd327ffb96 
--- a/Nominal/Ex/CPS/Lt.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/CPS/Lt.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -24,7 +24,6 @@
   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
   apply blast
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
-  apply blast
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
nominal2