--- 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}
+
*}