changeset 40436 | adb22dbb5242 |
parent 40327 | 1dfdbd66093a |
child 40484 | 768f7e264e2b |
--- a/src/HOLCF/LowerPD.thy Wed Nov 03 17:22:25 2010 -0700 +++ b/src/HOLCF/LowerPD.thy Fri Nov 05 15:15:28 2010 -0700 @@ -43,7 +43,7 @@ unfolding lower_le_def Rep_PDPlus by fast lemma lower_le_PDUnit_PDUnit_iff [simp]: - "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b" + "(PDUnit a \<le>\<flat> PDUnit b) = (a \<sqsubseteq> b)" unfolding lower_le_def Rep_PDUnit by fast lemma lower_le_PDUnit_PDPlus_iff: