equal
deleted
inserted
replaced
664 (fn prems => |
664 (fn prems => |
665 [ |
665 [ |
666 cut_facts_tac prems 1, |
666 cut_facts_tac prems 1, |
667 strip_tac 1, |
667 strip_tac 1, |
668 dtac (ax_flat RS spec RS spec RS mp) 1, |
668 dtac (ax_flat RS spec RS spec RS mp) 1, |
669 fast_tac ((HOL_cs addss (!simpset addsimps [minimal]))) 1 |
669 fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1 |
670 ]); |
670 ]); |
671 |
671 |
672 |
672 |
673 qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" |
673 qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" |
674 (fn prems => |
674 (fn prems => |