Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
installing the plus_ac0 axclass
authorpaulson
Wed, 24 May 2000 18:47:43 +0200
changeset 8959 9d793220a46a
parent 8958 ba75f564726b
child 8960 0cd01ec1830b
installing the plus_ac0 axclass
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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 **)
isabelle