# HG changeset patch
# User mueller
# Date 861894247 -7200
# Node ID c51ee445605da14c65f6da087420afc4021d9e46
# Parent  04e3359921a84dcf7c5fa1c40f05fc2d6fa9227f
added some comments;

diff -r 04e3359921a8 -r c51ee445605d src/HOLCF/Cfun3.ML
--- 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));*)