# HG changeset patch
# User wenzelm
# Date 1162990114 -3600
# Node ID 23e6eb4d09758db9030acf75311f3cc7a16fd693
# Parent  0e9d222db727d64ba2a9bc9725fcab3fc8993bc2
proper definition of add_zero_left/right;

diff -r 0e9d222db727 -r 23e6eb4d0975 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Nov 08 13:48:33 2006 +0100
+++ b/src/HOL/OrderedGroup.thy	Wed Nov 08 13:48:34 2006 +0100
@@ -101,6 +101,9 @@
   finally show ?thesis .
 qed
 
+lemmas add_zero_left = add_0
+  and add_zero_right = add_0_right
+
 lemma add_left_cancel [simp]:
      "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))"
 by (blast dest: add_left_imp_eq) 
@@ -1055,13 +1058,6 @@
 declare diff_le_0_iff_le [simp]
 
 
-
-
-ML {*
-val add_zero_left = thm"add_0";
-val add_zero_right = thm"add_0_right";
-*}
-
 ML {*
 val add_assoc = thm "add_assoc";
 val add_commute = thm "add_commute";