--- a/src/HOLCF/Library/List_Cpo.thy Sat Oct 02 17:50:33 2010 -0700
+++ b/src/HOLCF/Library/List_Cpo.thy Mon Oct 04 06:45:57 2010 -0700
@@ -133,7 +133,7 @@
assumes B: "range B <<| xs"
shows "range (\<lambda>i. A i # B i) <<| x # xs"
using assms
-unfolding is_lub_def is_ub_def Ball_def [symmetric]
+unfolding is_lub_def is_ub_def
by (clarsimp, case_tac u, simp_all)
instance list :: (cpo) cpo
--- a/src/HOLCF/Porder.thy Sat Oct 02 17:50:33 2010 -0700
+++ b/src/HOLCF/Porder.thy Mon Oct 04 06:45:57 2010 -0700
@@ -70,7 +70,7 @@
subsection {* Upper bounds *}
definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<|" 55) where
- "S <| x \<longleftrightarrow> (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
+ "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
by (simp add: is_ub_def)