--- a/src/HOLCF/Cfun3.ML Thu Apr 24 11:21:46 1997 +0200
+++ b/src/HOLCF/Cfun3.ML Thu Apr 24 17:04:07 1997 +0200
@@ -184,9 +184,9 @@
Addsimps cont_lemmas1;
+(* HINT: cont_tac is now installed in simplifier in Lift3.ML ! *)
(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
-
(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
(* ------------------------------------------------------------------------ *)
@@ -369,4 +369,5 @@
(* use cont_tac as autotac. *)
(* ------------------------------------------------------------------------ *)
+(* HINT: cont_tac is now installed in simplifier in Lift3.ML ! *)
(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)