--- 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}