--- a/CookBook/FirstSteps.thy Wed Jan 28 06:29:16 2009 +0000
+++ b/CookBook/FirstSteps.thy Wed Jan 28 06:43:51 2009 +0000
@@ -522,8 +522,8 @@
\begin{readmore}
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
- and @{ML_file "Pure/General/basics.ML"}. The section ?? in the implementation manual
- contains also information about combinators.
+ and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
+ contains further information about combinators.
\end{readmore}
The simplest combinator is @{ML I}, which is just the identity function.