CookBook/FirstSteps.thy
changeset 87 90189a97b3f8
parent 86 fdb9ea86c2a3
child 89 fee4942c4770
--- 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.