CookBook/FirstSteps.thy
changeset 73 bcbcf5c839ae
parent 72 7b8c4fe235aa
child 75 f2dea0465bb4
--- 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}
+
   
 *}