src/HOL/Finite.thy

--- a/src/HOL/Finite.thy	Fri Dec 04 10:40:06 1998 +0100
+++ b/src/HOL/Finite.thy	Fri Dec 04 10:42:53 1998 +0100
@@ -63,8 +63,6 @@
     f    :: ['b,'a] => 'a
   assumes
     lcomm    "f x (f y z) = f y (f x z)"
-  defines
-    (*nothing*)
 
 locale ACe =
   fixes 
@@ -74,6 +72,5 @@
     ident    "f x e = x"
     commute  "f x y = f y x"
     assoc    "f (f x y) z = f x (f y z)"
-  defines
 
 end