
diff -r d3d2b78b1c19 -r a8cc904a6820 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -128,7 +128,7 @@
   show "1 * a = a"
     by partiality_descending auto
   show "a + b + c = a + (b + c)"
-    by partiality_descending (auto simp add: mult_commute right_distrib)
+    by partiality_descending (auto simp add: mult_commute distrib_left)
   show "a + b = b + a"
     by partiality_descending auto
   show "0 + a = a"
@@ -138,7 +138,7 @@
   show "a - b = a + - b"
     by (simp add: minus_rat_def)
   show "(a + b) * c = a * c + b * c"
-    by partiality_descending (auto simp add: mult_commute right_distrib)
+    by partiality_descending (auto simp add: mult_commute distrib_left)
   show "(0 :: rat) \<noteq> (1 :: rat)"
     by partiality_descending auto
 qed




