--- 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)" *)