--- a/QuotMain.thy	Tue Oct 27 11:03:38 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 11:27:53 2009 +0100
@@ -15,9 +15,13 @@
 begin
 
 definition
+  ABS::"'a \<Rightarrow> 'b"
+where
   "ABS x \<equiv> Abs (R x)"
 
 definition
+  REP::"'b \<Rightarrow> 'a"
+where
   "REP a = Eps (Rep a)"
 
 lemma lem9:
@@ -100,19 +104,8 @@
   assumes ac: "R a c"
   and     bd: "R b d"
   shows "R a b = R c d"
-proof
-  assume "R a b"
-  then have "R b a" using R_sym by blast
-  then have "R b c" using ac R_trans by blast
-  then have "R c b" using R_sym by blast
-  then show "R c d" using bd R_trans by blast
-next
-  assume "R c d"
-  then have "R a d" using ac R_trans by blast
-  then have "R d a" using R_sym by blast
-  then have "R b a" using bd R_trans by blast
-  then show "R a b" using R_sym by blast
-qed
+using ac bd
+by (blast intro: R_trans R_sym)
 
 lemma REPS_same:
   shows "R (REP a) (REP b) \<equiv> (a = b)"