--- a/CookBook/Appendix.thy	Wed Jan 14 23:44:14 2009 +0000
+++ b/CookBook/Appendix.thy	Thu Jan 15 13:42:28 2009 +0000
@@ -7,7 +7,6 @@
 
 chapter {* Recipes *}
 
-
 end
   
 

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

--- a/CookBook/antiquote_setup.ML	Wed Jan 14 23:44:14 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Thu Jan 15 13:42:28 2009 +0000
@@ -23,8 +23,7 @@
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
  else
-    (*map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))*)
-    map (Output.output o Pretty.str_of)
+    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 

Binary file cookbook.pdf has changed