diff -r 46cc6708c3b3 -r fa810f01f7b5 Quot/Examples/Terms.thy
--- a/Quot/Examples/Terms.thy	Tue Jan 26 16:30:51 2010 +0100
+++ b/Quot/Examples/Terms.thy	Tue Jan 26 20:07:50 2010 +0100
@@ -62,7 +62,9 @@
 where
   a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)"
 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2"
-| a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> (fv_trm1 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> 
+                      (fv_trm1 t - {a})\<sharp>* pi \<and> 
+                      (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)
        \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s"
 | a4: "\<exists>pi::name prm.(
          t1 \<approx>1 t2 \<and>
@@ -125,7 +127,10 @@
 where
   a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
-| a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> (fv_trm2 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>2 s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> 
+                      (fv_trm2 t - {a})\<sharp>* pi \<and> 
+                      (pi \<bullet> t) \<approx>2 s \<and> 
+                      (pi \<bullet> a) = b)
        \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
 | a4: "\<exists>pi::name prm. (
          fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>