--- a/CookBook/FirstSteps.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/FirstSteps.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -248,11 +248,35 @@
   avoided: it is more than easy to get the intermediate values wrong, not to 
   mention the nightmares the maintenance of this code causes!
 
+  A ``real world'' example for a function written in the waterfall fashion might
+  be the following:
+*}
 
-  (FIXME: give a real world example involving theories)
+ML %linenosgray{*fun apply_fresh_args pred ctxt =
+  pred |> fastype_of
+       |> binder_types 
+       |> map (pair "z")
+       |> Variable.variant_frees ctxt [pred]
+       |> map Free  
+       |> (curry list_comb) pred *}
 
-  Similarly, the combinator @{ML "#>"} is the reverse function 
-  composition. It can be used to define the following function
+text {*
+  The point of this function is to extract the argument types of the given
+  predicate and then generate for each type a distinct variable; finally it
+  applies the generated variables to the predicate. You can read this off from
+  how the function is coded: in Line 2, the function @{ML fastype_of}
+  calculates the type of the predicate; in Line 3, @{ML binder_types} produces
+  the list of argument types; Line 4 pairs up each type with the string/name
+  @{text "z"}; the function @{ML variant_frees in Variable} generates for each
+  @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
+  is turned into a list of variable terms in Line 6, which in the last line
+  are applied by the function @{ML list_comb} to the predicate. We have to use
+  the function @{ML curry}, because @{ML list_comb} expects the predicate and
+  the argument list as a pair.
+
+  
+  The combinator @{ML "#>"} is the reverse function composition. It can be
+  used to define the following function
 *}
 
 ML{*val inc_by_six = 
@@ -800,7 +824,7 @@
   @{ML_response [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
-  However, efficiency is gained on the expense of skiping some tests. You 
+  However, efficiency is gained on the expense of skipping some tests. You 
   can see this in the following example
 
    @{ML_response [display,gray] 
@@ -944,8 +968,7 @@
   using the function @{ML Attrib.add_attributes} as follows.
 *}
 
-setup {*
-  Attrib.add_attributes 
+setup %gray {* Attrib.add_attributes 
     [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
 
 text {*
@@ -1012,10 +1035,9 @@
   and set up the attributes as follows
 *}
 
-setup {*
-  Attrib.add_attributes 
-    [("my_thms", Attrib.add_del_args my_add my_del, 
-        "maintaining a list of my_thms")] *}
+setup %gray {* Attrib.add_attributes 
+          [("my_thms", Attrib.add_del_args my_add my_del, 
+              "maintaining a list of my_thms")] *}
 
 text {*
   Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
@@ -1094,7 +1116,7 @@
   and set up the @{ML_struct FooRules} with the command
 *}
 
-setup {* FooRules.setup *}
+setup %gray {* FooRules.setup *}
 
 text {*
   This code declares a data slot where the theorems are stored,

--- a/CookBook/Intro.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Intro.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -108,7 +108,7 @@
   Further information or pointers to files.
   \end{readmore}
 
-  A few exercises a scattered around the text. Their solutions are given 
+  A few exercises are scattered around the text. Their solutions are given 
   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
   to solve the exercises on your own, and then look at the solutions.
 

--- a/CookBook/Package/Ind_Code.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -189,6 +189,8 @@
   set up the goals for the induction principles. 
 *}
 
+ML {* singleton *}
+ML {* ProofContext.export *}
 
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let

--- a/CookBook/Package/Ind_Interface.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -139,7 +139,7 @@
 in
   parse spec_parser input
 end"
-"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+"(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]),
      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}

--- a/CookBook/Package/Simple_Inductive_Package.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Package/Simple_Inductive_Package.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -31,7 +31,7 @@
 simple_inductive
   accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  accpartI: "(\<forall>y. r y x \<longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
+  accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x"
 
 thm accpart_def
 thm accpart.induct
@@ -53,9 +53,6 @@
 
 thm rel.accpartI'
 thm rel.accpart'.induct
-
-
-lemma "True" by simp
 *)
 
 use_chunks "simple_inductive_package.ML"

--- a/CookBook/Parsing.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Parsing.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -613,14 +613,6 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
-text {* and *}
-
-simple_inductive 
-  trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota> R x x"
-| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
-
 text {*
   For this we are going to use the parser:
 *}
@@ -628,7 +620,6 @@
 ML %linenosgray{*val spec_parser = 
      OuterParse.opt_target --
      OuterParse.fixes -- 
-     OuterParse.for_fixes --
      Scan.optional 
        (OuterParse.$$$ "where" |--
           OuterParse.!!! 
@@ -655,16 +646,16 @@
 in
   parse spec_parser input
 end"
-"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+"(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]),
      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 
-  As you see, the result is a ``nested'' four-tuple consisting of an 
-  optional locale (in this case @{ML NONE}); a list of variables with optional 
-  type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this
-  case there are none); and a list of rules where every rule has optionally a name and 
-  an attribute.
+  As you see, the result is a ``nested'' four-tuple consisting of an optional
+  locale (in this case @{ML NONE}); a list of variables with optional
+  type-annotation and syntax-annotation; and a list of rules where every rule
+  has optionally a name and an attribute.
+
 
   In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target 
   in order to indicate a locale in which the specification is made. For example
@@ -705,15 +696,7 @@
   The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
   \end{readmore}
 
-  Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the
-  same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, 
-  but requires that this list is prefixed by the keyword \isacommand{for}.
-
-@{ML_response [display,gray]
-"parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")"
-"([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"}  
-
-  Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a
+  Lines 4 to 8 in the function @{ML spec_parser} implement the parser for a
   list of introduction rules, that is propositions with theorem
   annotations. The introduction rules are propositions parsed by @{ML
   OuterParse.prop}. However, they can include an optional theorem name plus
@@ -729,7 +712,7 @@
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name 
   has to end with @{text [quotes] ":"}---see the argument of 
-  the function @{ML SpecParse.opt_thm_name} in Line 9.
+  the function @{ML SpecParse.opt_thm_name} in Line 8.
 
   \begin{readmore}
   Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} 

--- a/CookBook/Solutions.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Solutions.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -79,7 +79,7 @@
 
 text {* The setup for the simproc is *}
 
-simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}
+simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *}
  
 text {* and a test case is the lemma *}
 

--- a/CookBook/Tactical.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Tactical.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -524,6 +524,7 @@
 
 text_raw{*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
@@ -544,6 +545,7 @@
 end*}
 text_raw{*
 \end{isabelle}
+\end{minipage}
 \caption{A function that prints out the various parameters provided by the tactic
  @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
   extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
@@ -1120,6 +1122,7 @@
 
 text_raw {*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
@@ -1144,6 +1147,7 @@
 end*}
 text_raw {* 
 \end{isabelle}
+\end{minipage}
 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
@@ -1455,7 +1459,7 @@
   done by adding the simproc to the current simpset as follows
 *}
 
-simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
 
 text {*
   where the second argument specifies the pattern and the right-hand side
@@ -1539,7 +1543,7 @@
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1591,11 +1595,13 @@
 *}
 
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
   where the simproc produces the goal state
-
+  
+  \begin{minipage}{\textwidth}
   @{subgoals[display]}
+  \end{minipage}
 *}  
 (*<*)oops(*>*)
 
@@ -1694,11 +1700,13 @@
   *}
 
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
 txt {* 
   you obtain the more legible goal state
   
+  \begin{minipage}{\textwidth}
   @{subgoals [display]}
+  \end{minipage}
   *}
 (*<*)oops(*>*)
 
@@ -2025,7 +2033,9 @@
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
 
-       @{subgoals [display]}*}
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}*}
 (*<*)oops(*>*)
 
 text {*

--- a/CookBook/document/root.tex	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/document/root.tex	Sat Mar 14 00:48:22 2009 +0100
@@ -97,6 +97,10 @@
 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
 \renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}
 
+\isakeeptag{gray}
+\renewcommand{\isataggray}{\begin{graybox}}
+\renewcommand{\endisataggray}{\end{graybox}}
+
 \isakeeptag{small}
 \renewcommand{\isatagsmall}{\begingroup\small}
 \renewcommand{\endisatagsmall}{\endgroup}

Binary file cookbook.pdf has changed