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/LFex.thy
changeset 1264 1dedc0b76f32
parent 1259 db158e995bfc
child 1277 6eacf60ce41d 
--- a/Nominal/LFex.thy	Thu Feb 25 09:41:14 2010 +0100
+++ b/Nominal/LFex.thy	Thu Feb 25 12:15:11 2010 +0100
@@ -51,15 +51,12 @@
 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
 done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
nominal2