# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265111292 -3600
# Node ID 278253330b6ad3b55a7ac3cc9ef8fa14f26fb0a7
# Parent  559419060d99b70fa74bb58db1bb651ccb65a415
Disambiguating the syntax.

diff -r 559419060d99 -r 278253330b6a Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 02 12:36:01 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 02 12:48:12 2010 +0100
@@ -53,7 +53,7 @@
   "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)"
 
 notation
-  alpha_gen ("_ \<approx>gen _ _ _ _")
+  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
 
 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
   by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
@@ -71,7 +71,7 @@
 
 lemma alpha_gen_atom_sym:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow>
+  shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
         \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
   apply(erule exE)
   apply(rule_tac x="- pi" in exI)
@@ -97,7 +97,7 @@
 
 lemma alpha_gen_atom_trans:
   assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x) f pi ({atom aa}, ta);
+  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
         \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
     \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
   apply(simp add: alpha_gen.simps)
@@ -131,7 +131,7 @@
 
 lemma alpha_gen_atom_eqvt:
   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s)"
+  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
   shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
   using b apply -
   apply(erule exE)
diff -r 559419060d99 -r 278253330b6a Quot/Nominal/LamEx2.thy
--- 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])