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.
Quot/Nominal/LamEx2.thy
changeset 1026 278253330b6a
parent 1025 559419060d99
child 1028 41fc4d3fc764 
--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 12:36:01 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 12:48:12 2010 +0100
@@ -371,7 +371,7 @@
 lemma alpha_induct: 
   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
- \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
+ \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2) fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
 unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen])
nominal2