# HG changeset patch
# User haftmann
# Date 1203088150 -3600
# Node ID 046fe7ddfc4b0bbb0caedbd850fd767331815e95
# Parent  21b78307096f1d71ee68d6fec501c54db415396a
moved *_reorient lemmas here

diff -r 21b78307096f -r 046fe7ddfc4b src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Feb 15 14:20:51 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Feb 15 16:09:10 2008 +0100
@@ -75,6 +75,9 @@
   assumes add_0_left [simp]: "0 + a = a"
     and add_0_right [simp]: "a + 0 = a"
 
+lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
+  by (rule eq_commute)
+
 class comm_monoid_add = zero + ab_semigroup_add +
   assumes add_0: "0 + a = a"
 begin
@@ -88,6 +91,9 @@
   assumes mult_1_left [simp]: "1 * a  = a"
   assumes mult_1_right [simp]: "a * 1 = a"
 
+lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
+  by (rule eq_commute)
+
 class comm_monoid_mult = one + ab_semigroup_mult +
   assumes mult_1: "1 * a = a"
 begin