src/HOL/Algebra/poly/PolyRing.thy

--- a/src/HOL/Algebra/poly/PolyRing.thy	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/poly/PolyRing.thy	Fri Nov 10 19:15:38 2000 +0100
@@ -10,6 +10,6 @@
   up :: (ring) ring
   (up_a_assoc, up_l_zero, up_l_neg, up_a_comm, 
    up_m_assoc, up_l_one, up_l_distr, up_m_comm, up_one_not_zero,
-   up_power_def) {| rtac refl 1 |}
+   up_inverse_def, up_divide_def, up_power_def) {| ALLGOALS (rtac refl) |}
 
 end