changeset 14430 | 5cb24165a2e1 |
parent 14398 | c5c47703f763 |
child 14444 | 24724afce166 |
--- 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 *}