diff -r 7b8c4fe235aa -r bcbcf5c839ae CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Jan 14 23:44:14 2009 +0000 +++ b/CookBook/FirstSteps.thy Thu Jan 15 13:42:28 2009 +0000 @@ -575,7 +575,24 @@ section {* Combinators *} text {* - @{text I}, @{text K} + Perhaps one of the most puzzling aspects for a beginner when looking at + existing Isabelle code is the liberal use of combinators. At first they + seem to obstruct reading the code, but after getting familiar with them + they actually ease the reading and also the programming. + + \begin{readmore} + The most frequently used combinator are defined in @{ML_file "Pure/library.ML"} + and @{ML_file "Pure/General/basics.ML"}. + \end{readmore} + + The simplest combinator is @{ML I} which is just the identidy function. +*} + +ML{*fun I x = x*} + +text {* + Another frequently used combinator is @{ML K} + *}