added some comments;
authormueller
Thu, 24 Apr 1997 17:04:07 +0200
changeset 3031 c51ee445605d
parent 3030 04e3359921a8
child 3032 74c5f175aa8e
added some comments;
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));*)