tuned;

--- a/src/HOL/Algebra/abstract/Factor.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/abstract/Factor.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 25 November 1997
 *)
 
-open Factor;
-
 goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
 \  [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
 by (ftac factorial_prime 1);

--- a/src/HOL/Algebra/abstract/Ring.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/abstract/Ring.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -280,9 +280,8 @@
 by Auto_tac;
 qed "inverse_unique";
 
-Goalw [inverse_def, dvd_def]
-  "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
-by (Asm_simp_tac 1);
+Goal "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
+by (asm_full_simp_tac (simpset () addsimps [inverse_ax, dvd_def]) 1);
 by (Clarify_tac 1);
 by (rtac someI 1);
 by (rtac sym 1);

--- a/src/HOL/Algebra/abstract/RingHomo.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 15 April 1997
 *)
 
-open RingHomo;
-
 (* Ring homomorphism *)
 
 Goalw [homo_def]

--- a/src/HOL/Algebra/poly/LongDiv.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -118,8 +118,8 @@
 \    Ex (% (q, r). f = q * g + r & (r = <0> | deg r < deg g))";
 by (forw_inst_tac [("f", "f")] long_div_ring 1);
 by (etac exE 1);
-by (res_inst_tac [("x", "((%(q,r,k). (Ring.inverse(lcoeff g ^k) *s q)) x, \
-\  (%(q,r,k). Ring.inverse(lcoeff g ^k) *s r) x)")] exI 1);
+by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \
+\  (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1);
 by (Clarify_tac 1);
 by (Simp_tac 1);
 by (rtac conjI 1);

--- a/src/HOL/Algebra/poly/PolyRing.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/poly/PolyRing.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 22 January 1997
 *)
 
-open PolyRing;
-
 (* Properties of *s:
    Polynomials form a module *)
 

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

--- a/src/HOL/Algebra/poly/ProtoPoly.ML	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/poly/ProtoPoly.ML	Fri Nov 10 19:15:38 2000 +0100
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 9 December 1996
 *)
 
-open ProtoPoly;
-
 (* Rules for bound *)
 
 val prem = goalw ProtoPoly.thy [bound_def]

--- a/src/HOL/Algebra/poly/UnivPoly.thy	Fri Nov 10 19:15:14 2000 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly.thy	Fri Nov 10 19:15:38 2000 +0100
@@ -36,6 +36,8 @@
   up_zero_def	"<0> == Abs_UP (%x. <0>)"
   up_one_def	"<1> == monom 0"
   up_uminus_def	"- p == (-<1>) *s p"
+  up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else <0>)"
+  up_divide_def "(a::'a::ringS up) / b == a * inverse b"
   up_power_def	"a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n"
 end