diff -r 72a53b07d264 -r 0b24a016f6dd ProgTutorial/Tactical.thy --- 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}