# HG changeset patch
# User huffman
# Date 1199487407 -3600
# Node ID 3acdbb5626dc5c8de11e57f1daf386133a9a6482
# Parent  fe56cdb73ae56776f5395d715048707521143482
cleaned up some proofs

diff -r fe56cdb73ae5 -r 3acdbb5626dc src/HOLCF/Porder.thy
--- 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])