--- 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