# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269279539 -3600
# Node ID ed54632fab4a7718e80e10ac2293b9f18ba5ad4d
# Parent  f0028f13e5327c5fd1259a948845e983a0109be4
Marked the place where a compose lemma applies.

diff -r f0028f13e532 -r ed54632fab4a Nominal/Term5.thy
--- 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)