
diff -r 537206cc738f -r c2a4dccf6e67 src/HOL/AxClasses/Group/Group.thy
--- a/src/HOL/AxClasses/Group/Group.thy	Tue Oct 03 18:30:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title:      Group.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-Group = Sigs + Fun +
-
-(* semigroups *)
-
-axclass
-  semigroup < times
-  assoc         "(x * y) * z = x * (y * z)"
-
-
-(* groups *)
-
-axclass
-  group < one, inverse, semigroup
-  left_unit     "1 * x = x"
-  left_inverse  "inverse x * x = 1"
-
-
-(* abelian groups *)
-
-axclass
-  agroup < group
-  commut        "x * y = y * x"
-
-end




