src/HOLCF/Porder.thy
changeset 18088 e5b23b85e932
parent 18071 940c2c0ff33a
child 18647 5f5d37e763c4
--- a/src/HOLCF/Porder.thy	Fri Nov 04 22:26:09 2005 +0100
+++ b/src/HOLCF/Porder.thy	Fri Nov 04 22:27:40 2005 +0100
@@ -38,10 +38,7 @@
 by simp
 
 lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d"
-apply (erule trans_less)
-apply (erule trans_less)
-apply assumption
-done
+by (rule trans_less [OF trans_less])
 
 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)"
 by (fast elim!: antisym_less_inverse intro!: antisym_less)
@@ -128,11 +125,7 @@
 done
 
 lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
-apply (rule unique_lub)
-apply (rule lubI)
-apply assumption
-apply assumption
-done
+by (rule unique_lub [OF lubI])
 
 lemma lub_singleton [simp]: "lub {x} = x"
 by (simp add: thelubI is_lub_def is_ub_def)