# HG changeset patch
# User huffman
# Date 1215101739 -7200
# Node ID a89d755b029d010f5ed476c33a2b72d3d8df029b
# Parent  83f9734241169efbee8f8509c2cc1454005d511a
move proofs of add_left_cancel and add_right_cancel into the correct locale

diff -r 83f973424116 -r a89d755b029d src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu Jul 03 18:03:10 2008 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu Jul 03 18:15:39 2008 +0200
@@ -106,6 +106,17 @@
 class cancel_semigroup_add = semigroup_add +
   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
+begin
+
+lemma add_left_cancel [simp]:
+  "a + b = a + c \<longleftrightarrow> b = c"
+  by (blast dest: add_left_imp_eq)
+
+lemma add_right_cancel [simp]:
+  "b + a = c + a \<longleftrightarrow> b = c"
+  by (blast dest: add_right_imp_eq)
+
+end
 
 class cancel_ab_semigroup_add = ab_semigroup_add +
   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
@@ -125,19 +136,6 @@
 
 end
 
-context cancel_ab_semigroup_add
-begin
-
-lemma add_left_cancel [simp]:
-  "a + b = a + c \<longleftrightarrow> b = c"
-  by (blast dest: add_left_imp_eq)
-
-lemma add_right_cancel [simp]:
-  "b + a = c + a \<longleftrightarrow> b = c"
-  by (blast dest: add_right_imp_eq)
-
-end
-
 subsection {* Groups *}
 
 class group_add = minus + uminus + monoid_add +