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