src/HOLCF/Lift3.ML
changeset 5291 5706f0ef1d43
parent 5143 b94cd208f073
child 9245 428385c4bc50
--- a/src/HOLCF/Lift3.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -143,13 +143,13 @@
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
-qed"cont_fapp_app";
+qed"cont_Rep_CFun_app";
 
 Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
-by (etac cont_fapp_app 1);
+by (etac cont_Rep_CFun_app 1);
 by (assume_tac 1);
-qed"cont_fapp_app_app";
+qed"cont_Rep_CFun_app_app";
 
 
 (* continuity of if then else *)