# HG changeset patch
# User nipkow
# Date 1233159145 -3600
# Node ID cbe35f4f04f88c88dfef0c2fadff60770418299d
# Parent  2a580d9af918d8b0e88be30af678f059ad2a1825
removed spurious conflic msg

diff -r 2a580d9af918 -r cbe35f4f04f8 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Jan 28 16:57:36 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Wed Jan 28 17:12:25 2009 +0100
@@ -1202,7 +1202,6 @@
   qed
   have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
     by (simp add: abs_lattice le_supI)
-<<<<<<< local
   fix a b
   show "0 \<le> \<bar>a\<bar>" by simp
   show "a \<le> \<bar>a\<bar>"
@@ -1223,36 +1222,6 @@
       by (drule_tac abs_leI, auto)
     with g[symmetric] show ?thesis by simp
   qed
-=======
-  show ?thesis
-  proof
-    fix a
-    show "0 \<le> \<bar>a\<bar>" by simp
-  next
-    fix a
-    show "a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
-  next
-    fix a
-    show "\<bar>-a\<bar> = \<bar>a\<bar>" by (simp add: abs_lattice sup_commute)
-  next
-    fix a b
-    show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
-  next
-    fix a b
-    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
-    proof -
-      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
-        by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
-      have a:"a+b <= sup ?m ?n" by (simp)
-      have b:"-a-b <= ?n" by (simp) 
-      have c:"?n <= sup ?m ?n" by (simp)
-      from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
-      have e:"-a-b = -(a+b)" by (simp add: diff_minus)
-      from a d e have "abs(a+b) <= sup ?m ?n" by (drule_tac abs_leI, auto)
-      with g[symmetric] show ?thesis by simp
-    qed
-  qed auto
->>>>>>> other
 qed
 
 end