# HG changeset patch
# User paulson
# Date 959187088 -7200
# Node ID df06ec11bbfa24c8ce14c333661bd742b6e9a073
# Parent  0d4abacae6aacd3ce01ee971012f7eb63b7bc575
some lemmas about plus_ac0

diff -r 0d4abacae6aa -r df06ec11bbfa src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Wed May 24 18:50:08 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed May 24 18:51:28 2000 +0200
@@ -451,6 +451,20 @@
 by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
 qed "exCI";
 
+Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)";
+by (rtac (thm"plus_ac0.commute" RS trans) 1);
+by (rtac (thm"plus_ac0.assoc" RS trans) 1);
+by (rtac (thm"plus_ac0.commute" RS arg_cong) 1);
+qed "plus_ac0_left_commute";
+
+Goal "x + 0 = (x ::'a::plus_ac0)";
+by (rtac (thm"plus_ac0.commute" RS trans) 1);
+by (rtac (thm"plus_ac0.zero") 1);
+qed "plus_ac0_zero_right";
+
+bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute", 
+			plus_ac0_left_commute,
+			thm"plus_ac0.zero", plus_ac0_zero_right]);
 
 (* case distinction *)