--- a/Nominal/Manual/LamEx.thy	Thu Mar 25 20:12:57 2010 +0100
+++ b/Nominal/Manual/LamEx.thy	Fri Mar 26 09:23:23 2010 +0100
@@ -1,5 +1,5 @@
 theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs"
 begin
 
 atom_decl name
@@ -87,12 +87,12 @@
 done
 
 inductive
-    alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
+    alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
-| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)
-       \<Longrightarrow> rLam a t \<approx> rLam b s"
+  a1: "a = b \<Longrightarrow> (rVar a) \<approx>a (rVar b)"
+| a2: "\<lbrakk>t1 \<approx>a t2; s1 \<approx>a s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a rApp t2 s2"
+| a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s)
+       \<Longrightarrow> rLam a t \<approx>a rLam b s"
 
 lemma a3_inverse:
   assumes "rLam a t \<approx> rLam b s"