--- a/Nominal/Manual/LamEx.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Manual/LamEx.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -95,8 +95,8 @@
        \<Longrightarrow> rLam a t \<approx>a rLam b s"
 
 lemma a3_inverse:
-  assumes "rLam a t \<approx> rLam b s"
-  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)"
+  assumes "rLam a t \<approx>a rLam b s"
+  shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)"
 using assms
 apply(erule_tac alpha.cases)
 apply(auto)
@@ -104,7 +104,7 @@
 
 text {* should be automatic with new version of eqvt-machinery *}
 lemma alpha_eqvt:
-  shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
+  shows "t \<approx>a s \<Longrightarrow> (pi \<bullet> t) \<approx>a (pi \<bullet> s)"
 apply(induct rule: alpha.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -126,7 +126,7 @@
 done
 
 lemma alpha_refl:
-  shows "t \<approx> t"
+  shows "t \<approx>a t"
 apply(induct t rule: rlam.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -136,7 +136,7 @@
 done
 
 lemma alpha_sym:
-  shows "t \<approx> s \<Longrightarrow> s \<approx> t"
+  shows "t \<approx>a s \<Longrightarrow> s \<approx>a t"
 apply(induct rule: alpha.induct)
 apply(simp add: a1)
 apply(simp add: a2)
@@ -152,7 +152,7 @@
 done
 
 lemma alpha_trans:
-  shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
+  shows "t1 \<approx>a t2 \<Longrightarrow> t2 \<approx>a t3 \<Longrightarrow> t1 \<approx>a t3"
 apply(induct arbitrary: t3 rule: alpha.induct)
 apply(erule alpha.cases)
 apply(simp_all)
@@ -188,22 +188,22 @@
   done
 
 lemma alpha_rfv:
-  shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
+  shows "t \<approx>a s \<Longrightarrow> rfv t = rfv s"
   apply(induct rule: alpha.induct)
   apply(simp_all)
   done
 
 inductive
-    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+    alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a2 _" [100, 100] 100)
 where
-  a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
-| a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
-| a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+  a21: "a = b \<Longrightarrow> (rVar a) \<approx>a2 (rVar b)"
+| a22: "\<lbrakk>t1 \<approx>a2 t2; s1 \<approx>a2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a2 rApp t2 s2"
+| a23: "(a = b \<and> t \<approx>a2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>a2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>a2 rLam b s"
 
 lemma fv_vars:
   fixes a::name
   assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"
-  shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
+  shows "(pi \<bullet> t) \<approx>a2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
 using a1
 apply(induct t)
 apply(auto)
@@ -222,8 +222,8 @@
 
 
 lemma 
-  assumes a1: "t \<approx>2 s"
-  shows "t \<approx> s"
+  assumes a1: "t \<approx>a2 s"
+  shows "t \<approx>a s"
 using a1
 apply(induct)
 apply(rule alpha.intros)
@@ -254,8 +254,8 @@
 sorry
 
 lemma 
-  assumes a1: "t \<approx> s"
-  shows "t \<approx>2 s"
+  assumes a1: "t \<approx>a s"
+  shows "t \<approx>a2 s"
 using a1
 apply(induct)
 apply(rule alpha2.intros)
@@ -445,12 +445,12 @@
 done
 
 lemma rlam_distinct:
-  shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
-  and   "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
-  and   "\<not>(rVar nam \<approx> rLam nam' rlam')"
-  and   "\<not>(rLam nam' rlam' \<approx> rVar nam)"
-  and   "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
-  and   "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
+  shows "\<not>(rVar nam \<approx>a rApp rlam1' rlam2')"
+  and   "\<not>(rApp rlam1' rlam2' \<approx>a rVar nam)"
+  and   "\<not>(rVar nam \<approx>a rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx>a rVar nam)"
+  and   "\<not>(rApp rlam1 rlam2 \<approx>a rLam nam' rlam')"
+  and   "\<not>(rLam nam' rlam' \<approx>a rApp rlam1 rlam2)"
 apply auto
 apply (erule alpha.cases)
 apply (simp_all only: rlam.distinct)