ProgTutorial/Tactical.thy
changeset 384 0b24a016f6dd
parent 378 8d160d79b48c
child 388 0b337dedc306
--- a/ProgTutorial/Tactical.thy	Tue Nov 10 12:17:08 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Nov 11 05:34:46 2009 +0100
@@ -2482,7 +2482,8 @@
   \end{exercise}
 
   \begin{readmore}
-  See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 
+  See @{ML_file "Pure/conv.ML"} and  @{ML_file "Tools/more_conv.ML"}
+  for more information about conversion combinators. 
   Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
   \end{readmore}