diff -r cc951743c5e2 -r a6a4c88e1c9a Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 15:25:24 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 15:36:29 2010 +0100
@@ -17,7 +17,7 @@
 | rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
 
 overloading
-  perm_rlam    \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam"   (unchecked)
+  perm_rlam \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam"   (unchecked)
 begin
 
 fun
@@ -63,7 +63,7 @@
 
 
 quotient_definition
-   "Var :: name \<Rightarrow> lam"
+  "Var :: name \<Rightarrow> lam"
 as
   "rVar"
 
@@ -73,12 +73,12 @@
   "rApp"
 
 quotient_definition
-   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
+  "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
 as
   "rLam"
 
 quotient_definition
-   "fv :: lam \<Rightarrow> name set"
+  "fv :: lam \<Rightarrow> name set"
 as
   "rfv"
 
@@ -155,10 +155,10 @@
 
 lemma rVar_rsp[quot_respect]:
   "(op = ===> alpha) rVar rVar"
-by (auto intro: a1)
+  by (auto intro: a1)
 
 lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp"
-by (auto intro: a2)
+  by (auto intro: a2)
 
 lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
@@ -172,11 +172,10 @@
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
-apply (auto)
-apply (erule alpha.cases)
-apply (simp_all add: rlam.inject alpha_refl)
-done
-
+  apply (auto)
+  apply (erule alpha.cases)
+  apply (simp_all add: rlam.inject alpha_refl)
+  done
 
 lemma pi_var1:
   fixes pi::"'x prm"