diff -r 9f6c606d5b59 -r 3acc7d25627a Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Feb 10 11:09:30 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Feb 10 11:27:49 2010 +0100
@@ -70,28 +70,28 @@
 
 theorem thm11:
   shows "R r r' = (abs r = abs r')"
-unfolding abs_def
-by (simp only: equivp[simplified equivp_def] lem7)
+  unfolding abs_def
+  by (simp only: equivp[simplified equivp_def] lem7)
 
 lemma rep_refl:
   shows "R (rep a) (rep a)"
-unfolding rep_def
-by (simp add: equivp[simplified equivp_def])
+  unfolding rep_def
+  by (simp add: equivp[simplified equivp_def])
 
 
 lemma rep_abs_rsp:
   shows "R f (rep (abs g)) = R f g"
   and   "R (rep (abs g)) f = R g f"
-by (simp_all add: thm10 thm11)
+  by (simp_all add: thm10 thm11)
 
 lemma Quotient:
   shows "Quotient R abs rep"
-unfolding Quotient_def
-apply(simp add: thm10)
-apply(simp add: rep_refl)
-apply(subst thm11[symmetric])
-apply(simp add: equivp[simplified equivp_def])
-done
+  unfolding Quotient_def
+  apply(simp add: thm10)
+  apply(simp add: rep_refl)
+  apply(subst thm11[symmetric])
+  apply(simp add: equivp[simplified equivp_def])
+  done
 
 end
 
@@ -142,10 +142,10 @@
   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
-by (simp_all add: Quot_True_def ext)
+  by (simp_all add: Quot_True_def ext)
 
 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
-by (simp add: Quot_True_def)
+  by (simp add: Quot_True_def)
 
 text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"