# HG changeset patch
# User huffman
# Date 1286199957 25200
# Node ID d841744718fec1775f7f582a9077a3376ebfb0e0
# Parent  1c6dce3ef477fb929bf4303ea5f8ad138a6d7ad5
define is_ub predicate using bounded quantifier

diff -r 1c6dce3ef477 -r d841744718fe src/HOLCF/Library/List_Cpo.thy
--- 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
diff -r 1c6dce3ef477 -r d841744718fe src/HOLCF/Porder.thy
--- 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)