equal
deleted
inserted
replaced
520 comprehension of the code, but after getting familiar with them, they |
520 comprehension of the code, but after getting familiar with them, they |
521 actually ease the understanding and also the programming. |
521 actually ease the understanding and also the programming. |
522 |
522 |
523 \begin{readmore} |
523 \begin{readmore} |
524 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
524 The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} |
525 and @{ML_file "Pure/General/basics.ML"}. The section ?? in the implementation manual |
525 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} |
526 contains also information about combinators. |
526 contains further information about combinators. |
527 \end{readmore} |
527 \end{readmore} |
528 |
528 |
529 The simplest combinator is @{ML I}, which is just the identity function. |
529 The simplest combinator is @{ML I}, which is just the identity function. |
530 *} |
530 *} |
531 |
531 |