diff -r 0fce2d8bce0f -r 5cb24165a2e1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 04 12:06:07 2004 +0100
@@ -197,11 +197,6 @@
 syntax (HTML output)
   abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
 
-axclass plus_ac0 < plus, zero
-  commute: "x + y = y + x"
-  assoc:   "(x + y) + z = x + (y + z)"
-  zero:    "0 + x = x"
-
 
 subsection {* Theory and package setup *}