diff -r fdb9ea86c2a3 -r 90189a97b3f8 CookBook/FirstSteps.thy --- 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.