# HG changeset patch
# User wenzelm
# Date 973880114 -3600
# Node ID 1dbd79bd3bc69a48a177b837b840248333abbcb7
# Parent  e7a8fc009d378ddcce9b85340ecbaaf1b3a5840b
use inverse, divide from basic HOL;

diff -r e7a8fc009d37 -r 1dbd79bd3bc6 src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Fri Nov 10 19:13:29 2000 +0100
+++ b/src/HOL/Algebra/abstract/Ring.thy	Fri Nov 10 19:15:14 2000 +0100
@@ -9,7 +9,7 @@
 (* Syntactic class ring *)
 
 axclass
-  ringS < plus, minus, times, power
+  ringS < plus, minus, times, power, inverse
 
 consts
   (* Basic rings *)
@@ -22,13 +22,8 @@
   irred		:: 'a::ringS => bool
   prime		:: 'a::ringS => bool
 
-  (* Fields *)
-  inverse	:: 'a::ringS => 'a
-  "'/"		:: ['a, 'a] => 'a::ringS		(infixl 70)
-
 translations
   "a -- b" 	== "a + (-b)"
-  "a / b"	== "a * inverse b"
 
 (* Class ring and ring axioms *)
 
@@ -50,6 +45,8 @@
   one_not_zero	"<1> ~= <0>"
   		(* if <1> = <0>, then the ring has only one element! *)
 
+  inverse_ax    "inverse a = (if a dvd <1> then @x. a*x = <1> else <0>)"
+  divide_ax     "a / b = a * inverse b"
   power_ax	"a ^ n = nat_rec <1> (%u b. b * a) n"
 
 defs
@@ -59,8 +56,6 @@
   prime_def	"prime p == p ~= <0> & ~ p dvd <1>
                           & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
 
-  inverse_def	"inverse a == if a dvd <1> then @x. a*x = <1> else <0>"
-
 (* Integral domains *)
 
 axclass