# HG changeset patch
# User huffman
# Date 1131139660 -3600
# Node ID e5b23b85e9324b4bbb14535d61925116d35435d6
# Parent  577d57e51f899f692d63c72dd331abd44eacf16e
cleaned up

diff -r 577d57e51f89 -r e5b23b85e932 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri Nov 04 22:26:09 2005 +0100
+++ b/src/HOLCF/Cont.thy	Fri Nov 04 22:27:40 2005 +0100
@@ -92,10 +92,8 @@
 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"
 apply (rule contI)
 apply (rule thelubE)
-apply (erule ch2ch_monofun)
-apply assumption
-apply (erule contlubE [symmetric])
-apply assumption
+apply (erule (1) ch2ch_monofun)
+apply (erule (1) contlubE [symmetric])
 done
 
 text {* first a lemma about binary chains *}
@@ -115,7 +113,7 @@
 
 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
 apply (rule monofunI)
-apply (drule binchain_cont, assumption)
+apply (drule (1) binchain_cont)
 apply (drule_tac i=0 in is_ub_lub)
 apply simp
 done
@@ -128,8 +126,7 @@
 lemma cont2contlub: "cont f \<Longrightarrow> contlub f"
 apply (rule contlubI)
 apply (rule thelubI [symmetric])
-apply (erule contE)
-apply assumption
+apply (erule (1) contE)
 done
 
 lemmas cont2contlubE = cont2contlub [THEN contlubE]
@@ -190,8 +187,7 @@
 apply (rule monocontlub2cont)
 apply (erule monofun_lub_fun)
 apply (simp add: cont2mono)
-apply (erule contlub_lub_fun)
-apply assumption
+apply (erule (1) contlub_lub_fun)
 done
 
 lemma cont2cont_lub:
@@ -231,18 +227,16 @@
 done
 
 lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. (\<lambda>y. f x y))"
-apply (rule cont2cont_CF1L_rev)
-apply simp
-done
+by (rule cont2cont_CF1L_rev, simp)
 
 text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
 
 lemma contlub_abstraction:
   "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
     (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
+apply (drule cont2cont_CF1L_rev)
 apply (rule thelub_fun [symmetric])
-apply (rule ch2ch_cont)
-apply (erule (1) cont2cont_CF1L_rev)
+apply (erule (1) ch2ch_cont)
 done
 
 lemma mono2mono_app:
diff -r 577d57e51f89 -r e5b23b85e932 src/HOLCF/Porder.thy
--- 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)