src/HOLCF/ConvexPD.thy

--- a/src/HOLCF/ConvexPD.thy	Wed Nov 03 17:22:25 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Fri Nov 05 15:15:28 2010 -0700
@@ -33,7 +33,7 @@
 unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
 
 lemma convex_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<natural> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
 
 lemma convex_le_PDUnit_lemma1: