# HG changeset patch
# User paulson
# Date 959186863 -7200
# Node ID 9d793220a46a11f25e933f7383de4bca9cad23f0
# Parent  ba75f564726b9b18e0ee33680e10195d63945258
installing the plus_ac0 axclass

diff -r ba75f564726b -r 9d793220a46a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed May 24 18:46:38 2000 +0200
+++ b/src/HOL/HOL.thy	Wed May 24 18:47:43 2000 +0200
@@ -68,6 +68,10 @@
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)
 
+axclass plus_ac0 < plus, zero
+    commute: "x + y = y + x"
+    assoc:   "(x + y) + z = x + (y + z)"
+    zero:    "0 + x = x"
 
 
 (** Additional concrete syntax **)