# HG changeset patch
# User oheimb
# Date 902928695 -7200
# Node ID 410417e0fd04d2e3ffe456b23699d64cc66d130f
# Parent  bdef7d349d2713adf6776350839560beeff2cb62
repaired proof of chfindom_monofun2cont

diff -r bdef7d349d27 -r 410417e0fd04 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Wed Aug 12 15:29:34 1998 +0200
+++ b/src/HOLCF/Cont.ML	Wed Aug 12 15:31:35 1998 +0200
@@ -670,27 +670,24 @@
 	]);
 
 
-qed_goal "chfindom_monofun2cont" thy  "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
-(fn prems => 
-	[
-	cut_facts_tac prems 1,
-	rtac monocontlub2cont 1,
-	 atac 1,
-	rtac contlubI 1,
-	strip_tac 1,
-	forward_tac [chfin2finch] 1,
-	rtac antisym_less 1,
-	 fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun]) 
-	     addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1,
-	dtac (monofun_finch2finch COMP swap_prems_rl) 1,
-	 atac 1,
-	asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1,
-	etac conjE 1, etac exE 1,
-	asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1,
-	etac (monofunE RS spec RS spec RS mp) 1,
-	etac is_ub_thelub 1
-	]);
-
+Goal "monofun f ==> cont(f::'a::chfin=>'b::pcpo)";
+by(rtac monocontlub2cont 1);
+by( atac 1);
+by(rtac contlubI 1);
+by(strip_tac 1);
+by(forward_tac [chfin2finch] 1);
+by(rtac antisym_less 1);
+by( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
+               HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);
+by(dtac (monofun_finch2finch COMP swap_prems_rl) 1);
+by( atac 1);
+by(asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1);
+by(etac conjE 1);
+by(etac exE 1);
+by(asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1);
+by(etac (monofunE RS spec RS spec RS mp) 1);
+by(etac is_ub_thelub 1);
+qed "chfindom_monofun2cont";
 
 bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)