src/HOLCF/LowerPD.thy
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: