src/HOLCF/Lift3.ML
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)";