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.
Marked the place where a compose lemma applies.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 22 Mar 2010 18:38:59 +0100
changeset 1583 ed54632fab4a
parent 1582 f0028f13e532
child 1584 67936ae78997
child 1587 b6da798cef68
Marked the place where a compose lemma applies.
Nominal/Term5.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Term5.thy	Mon Mar 22 18:29:57 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 18:38:59 2010 +0100
@@ -113,6 +113,7 @@
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+(* HERE *)
 apply (simp add: alpha_gen)
 apply clarify
 apply(simp add: fresh_star_plus)
nominal2