--- a/QuotMain.thy	Sun Sep 20 05:18:36 2009 +0100
+++ b/QuotMain.thy	Sun Sep 20 05:48:49 2009 +0100
@@ -64,11 +64,7 @@
 lemma REP_ABS_rsp:
   shows "R f (REP (ABS g)) = R f g"
   and   "R (REP (ABS g)) f = R g f"
-apply(subst thm11)
-apply(simp add: thm10 thm11)
-apply(subst thm11)
-apply(simp add: thm10 thm11)
-done
+by (simp_all add: thm10 thm11)
 
 lemma QUOTIENT:
   "QUOTIENT R ABS REP"
@@ -103,13 +99,13 @@
   and     bd: "R b d"
   shows "R a b = R c d"
 proof
-  assume ab: "R a b"
+  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 ccd: "R c d"
+  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
@@ -121,17 +117,15 @@
 proof
   assume as: "R (REP a) (REP b)"
   from rep_prop
-  obtain x where eq: "Rep a = R x" by auto
-  (*also ... not useful in the proof  *) 
-  from rep_prop
-  obtain y where eq2: "Rep b = R y" by auto
-  then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp
+  obtain x y 
+    where eqs: "Rep a = R x" "Rep b = R y" by blast
+  from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
   then have "R x (Eps (R y))" using lem9 by simp
   then have "R (Eps (R y)) x" using R_sym by blast
   then have "R y x" using lem9 by simp
   then have "R x y" using R_sym by blast
   then have "ABS x = ABS y" using thm11 by simp
-  then have "Abs (Rep a) = Abs (Rep b)" using eq eq2 unfolding ABS_def by simp
+  then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
   then show "a = b" using rep_inverse by simp
 next
   assume ab: "a = b"
@@ -714,7 +708,7 @@
 
 lemma
   shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
-         ((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
+         ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
 unfolding IN_def INSERT_def
 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)