--- 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";