installing the plus_ac0 axclass
authorpaulson
Wed May 24 18:47:43 2000 +0200 (2000-05-24)
changeset 89599d793220a46a
parent 8958 ba75f564726b
child 8960 0cd01ec1830b
installing the plus_ac0 axclass
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed May 24 18:46:38 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed May 24 18:47:43 2000 +0200
     1.3 @@ -68,6 +68,10 @@
     1.4    *             :: "['a::times, 'a] => 'a"          (infixl 70)
     1.5    (*See Nat.thy for "^"*)
     1.6  
     1.7 +axclass plus_ac0 < plus, zero
     1.8 +    commute: "x + y = y + x"
     1.9 +    assoc:   "(x + y) + z = x + (y + z)"
    1.10 +    zero:    "0 + x = x"
    1.11  
    1.12  
    1.13  (** Additional concrete syntax **)