# HG changeset patch
# User nipkow
# Date 1233220105 -3600
# Node ID 16c8799e6a21d36f21a9af848b215cbe87b7e440
# Parent  c82a76a66e806aeadb50610811df4250f820fbd2# Parent  07f3da9fd2a00041843aec9e29575e445a975f33
merged

diff -r c82a76a66e80 -r 16c8799e6a21 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Wed Jan 28 21:49:25 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy	Thu Jan 29 10:08:25 2009 +0100
@@ -304,9 +304,9 @@
 
 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
 by (rule aci_convex_plus.mult_left_idem)
-
+(*
 lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
-
+*)
 lemma convex_unit_less_plus_iff [simp]:
   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
  apply (rule iffI)
diff -r c82a76a66e80 -r 16c8799e6a21 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Wed Jan 28 21:49:25 2009 +0100
+++ b/src/HOLCF/LowerPD.thy	Thu Jan 29 10:08:25 2009 +0100
@@ -258,9 +258,9 @@
 
 lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
 by (rule aci_lower_plus.mult_left_idem)
-
+(*
 lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
-
+*)
 lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
 apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
 apply (simp add: PDPlus_lower_less)
diff -r c82a76a66e80 -r 16c8799e6a21 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Jan 28 21:49:25 2009 +0100
+++ b/src/HOLCF/UpperPD.thy	Thu Jan 29 10:08:25 2009 +0100
@@ -256,9 +256,9 @@
 
 lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
 by (rule aci_upper_plus.mult_left_idem)
-
+(*
 lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
-
+*)
 lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
 apply (simp add: PDPlus_upper_less)