changeset 7499 | 23e090051cb8 |
parent 7322 | d16d7ddcc842 |
child 8935 | 548901d05a0e |
--- a/src/HOLCF/Cont.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/Cont.ML Tue Sep 07 10:40:58 1999 +0200 @@ -675,7 +675,7 @@ by ( atac 1); by (rtac contlubI 1); by (strip_tac 1); -by (forward_tac [chfin2finch] 1); +by (ftac 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);