changeset 29672 | 07f3da9fd2a0 |
parent 29511 | 7071b017cb35 |
child 29990 | b11793ea15a3 |
--- a/src/HOLCF/UpperPD.thy Wed Jan 28 17:12:25 2009 +0100 +++ b/src/HOLCF/UpperPD.thy Thu Jan 29 10:07:43 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)