src/HOLCF/Cfun3.ML
changeset 4004 773f3c061777
parent 3842 b55686a7b22c
child 4098 71e05eb27fb6
--- a/src/HOLCF/Cfun3.ML	Fri Oct 24 18:10:51 1997 +0200
+++ b/src/HOLCF/Cfun3.ML	Sat Oct 25 14:39:25 1997 +0200
@@ -184,7 +184,7 @@
 
 Addsimps cont_lemmas1;
 
-(* HINT: cont_tac is now installed in simplifier in Lift3.ML ! *)
+(* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
 
 (*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
 (*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
@@ -369,7 +369,7 @@
 (* use cont_tac as autotac.                                                *)
 (* ------------------------------------------------------------------------ *)
 
-(* HINT: cont_tac is now installed in simplifier in Lift3.ML ! *)
+(* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
 (*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
 
 (* ------------------------------------------------------------------------ *)