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/Abs.thy
changeset 2104 2205b572bc9b
parent 2092 c0ab7451b20d
child 2124 a17b25cb94a6 
--- a/Nominal/Abs.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Abs.thy	Tue May 11 17:16:57 2010 +0200
@@ -760,7 +760,7 @@
   by (simp_all add: fresh_plus_perm)
 
 
-lemma alpha_gen_eqvt(*[eqvt]*):
+lemma alpha_gen_eqvt[eqvt]:
   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
nominal2