changeset 4477 | b3e5857d8d99 |
parent 4098 | 71e05eb27fb6 |
child 4833 | 2e53109d4bc8 |
--- a/src/HOLCF/Lift3.ML Tue Dec 23 11:56:09 1997 +0100 +++ b/src/HOLCF/Lift3.ML Wed Dec 24 10:02:30 1997 +0100 @@ -148,7 +148,7 @@ goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)"; by (rtac cont2cont_CF1L 1); by (REPEAT (resolve_tac cont_lemmas1 1)); -by (Auto_tac()); +by Auto_tac; qed"cont_fapp_app"; goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";