src/HOLCF/Porder.thy
changeset 25834 3acdbb5626dc
parent 25828 228c53fdb3b4
child 25878 bfd53f791c10
--- a/src/HOLCF/Porder.thy	Fri Jan 04 23:24:32 2008 +0100
+++ b/src/HOLCF/Porder.thy	Fri Jan 04 23:56:47 2008 +0100
@@ -146,13 +146,13 @@
 by (rule unique_lub [OF lubI])
 
 lemma is_lub_singleton: "{x} <<| x"
-by (simp add: is_lub_def is_ub_def)
+by (simp add: is_lub_def)
 
 lemma lub_singleton [simp]: "lub {x} = x"
 by (rule thelubI [OF is_lub_singleton])
 
 lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
-by (simp add: is_lub_def is_ub_def)
+by (simp add: is_lub_def)
 
 lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
 by (rule is_lub_bin [THEN thelubI])