--- a/src/HOL/ex/Ring.thy Fri Nov 29 15:07:27 1996 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: HOL/ex/Ring.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Bits of rings.
-Main output: a simplification tactic for commutative rings.
-*)
-
-Ring = Group +
-
-(* Ring *)
-
-axclass ring < add_agroup, times
- times_assoc "(x*y)*z = x*(y*z)"
- distribL "x*(y+z) = x*y + x*z"
- distribR "(x+y)*z = x*z + y*z"
-
-(* Commutative ring *)
-
-axclass cring < ring
- times_commute "x*y = y*x"
-
-end