# HG changeset patch
# User bauerg
# Date 974412778 -3600
# Node ID e7a5e8d63394b1f3a7545033dd2876e116a0b9db
# Parent  97247fd6f1f85488599035a68b9e76fd2b0ec877
rings and fields;

diff -r 97247fd6f1f8 -r e7a5e8d63394 src/HOL/Library/Ring_and_Field.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Ring_and_Field.thy	Thu Nov 16 23:12:58 2000 +0100
@@ -0,0 +1,32 @@
+(*  Title:      HOL/Library/Ring_and_Field.thy
+    ID:         $Id$
+    Author:     Gertrud Bauer, TU Muenchen
+*)
+
+header {*
+  \title{Rings and Fields}
+  \author{Gertrud Bauer}
+*}
+
+theory Ring_and_Field = Main: 
+
+
+axclass ring < plus, minus, times, number
+  add_assoc: "(a + b) + c = a + (b + c)"
+  add_commute: "a + b = b + a"
+  left_zero: "#0 + a = a"
+  left_neg: "(- a) + a = #0"
+  minus_uminus: "a - b = a + (- b)"
+
+  mult_assoc: "(a * b) * c = a * (b * c)"
+  mult_commute: "a * b = b * a"
+  left_one: "#1 * a = a"
+
+  left_distrib: "(a + b) * c = a * c + b * c"
+
+
+axclass field < ring, inverse
+  left_inverse: "a \<noteq> #0 \<Longrightarrow> inverse a * a = #1"
+  divides_inverse: "a / b = a * inverse b"
+
+end
\ No newline at end of file