--- a/CookBook/FirstSteps.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -226,17 +226,17 @@
 
   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
-  Consider for example
+  Consider for example the pairs
 
   @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
  
-  which inserts the coercion in the second component and 
+  where an coercion is inserted in the second component and 
 
   @{ML_response [display] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 
-  which does not (since it is already constructed using the meta-implication). 
+  where it is not (since it is already constructed using the meta-implication). 
 
   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
 
@@ -281,36 +281,39 @@
 
 text {*
   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
-  to both functions: 
+  to both functions. With @{ML make_imp} we obtain the correct term involving 
+  @{term "S"}, @{text "T"} and  @{text "@{typ nat}"} 
 
   @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" 
     "Const \<dots> $ 
     Abs (\"x\", Type (\"nat\",[]),
       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
                   (Free (\"T\",\<dots>) $ \<dots>))"}
+
+  With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} 
+  and @{text "Q"} from the antiquotation.
+
   @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
     "Const \<dots> $ 
     Abs (\"x\", \<dots>,
       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  As can be seen, in the first case the arguments are correctly used, while the 
-  second generates a term involving the @{term "P"} and @{text "Q"} from the 
-  antiquotation.
+  One tricky point in constructing terms by hand is to obtain the fully
+  qualified name for constants. For example the names for @{text "zero"} and
+  @{text "+"} are more complex than one first expects, namely
 
-  One tricky point in constructing terms by hand is to obtain the 
-  fully qualified name for constants. For example the names for @{text "zero"} and
-  @{text "+"} are more complex than one first expects, namely 
 
   \begin{center}
   @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. 
   \end{center}
   
-  The extra prefixes @{text zero_class} and @{text plus_class} are present because 
-  these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
-  which theory they are defined. Guessing such internal names can sometimes be quite hard. 
-  Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
-  expansion automatically, for example:
+  The extra prefixes @{text zero_class} and @{text plus_class} are present
+  because these constants are defined within type classes; the prefix @{text
+  "HOL"} indicates in which theory they are defined. Guessing such internal
+  names can sometimes be quite hard. Therefore Isabelle provides the
+  antiquotation @{text "@{const_name \<dots>}"} which does the expansion
+  automatically, for example:
 
   @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
 
@@ -575,6 +578,11 @@
 section {* Theorem Attributes *}
 
 
+section {* Combinators *}
 
+text {*
+  @{text I}, @{text K}
+  
+*}
 
 end
\ No newline at end of file

--- a/CookBook/Intro.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Intro.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -64,5 +64,12 @@
 
 *}
 
+section {* Conventions *}
+
+text {*
+  We use @{text "$"} to indicate a command needs to be run on the Unix-command
+  line.
+*}
+
 
 end
\ No newline at end of file

--- a/CookBook/Parsing.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -1,5 +1,5 @@
 theory Parsing
-imports Base
+imports Base 
 
 begin
 
@@ -556,70 +556,78 @@
 section {* New Commands and Creating Keyword Files *}
 
 text {*
-  Often new commands, for example for providing a new definitional principle,
-  need to be programmed. While this is not difficult to do on the ML-level,
+  Often new commands, for example for providing new definitional principles,
+  need to be implemented. While this is not difficult on the ML-level,
   new commands, in order to be useful, need to be recognised by
   ProofGeneral. This results in some subtle configuration issues, which we
   will explain in this section.
 
-  Let us start with a ``silly'' command, which we call \isacommand{foo} in what follows.
+  Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows.
   To keep things simple this command does nothing at all. On the ML-level it can be defined as
+*}
 
-@{ML [display]
-"let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+ML {* 
+let
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+  OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end 
+*}
 
+text {*
   The function @{ML OuterSyntax.command} expects a name for the command, a
-  short description, a flag (which we will explain later on more thoroughly) and a
+  short description, a kind indicator (which we will explain later on more thoroughly) and a
   parser for a top-level transition function (its purpose will also explained
   later). 
 
-  While this is everything we have to do on the ML-level, we need 
-  now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral 
-  to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with 
-  the command-line
+  While this is everything we have to do on the ML-level, we need a keyword
+  file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
+  recognise \isacommand{foobar} as a command. Such a keyword file can be
+  generated with the command-line
+
+
+  @{text [display] "$ isabelle keywords -k foobar some-log-files"}
 
-  @{text [display] "$ isabelle keywords -k foo <some-log-files>"}
+  The option @{text "-k foobar"} indicates which postfix the keyword file will
+  obtain. In the case above the generated file will be named @{text
+  "isar-keywords-foobar.el"}. However, this command requires log files to be
+  present (in order to extract the keywords from them). To generate these log
+  files, we first package the code above into a separate theory file named
+  @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
+  complete code.
 
-  The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
-  the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command
-  requires log files to be present (in order to extract the keywords from them). 
-  To generate these log files, we first package the code above into a separate theory file 
-  named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. 
 
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{figure}[t]
-  \begin{boxedminipage}{\textwidth}
+  \begin{boxedminipage}{\textwidth}\small
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
   \isacommand{ML}~\isa{\isacharverbatimopen}\\
   @{ML
 "let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
+  OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
   \isa{\isacharverbatimclose}\\
   \isacommand{end}
   \end{boxedminipage}
   \caption{The file @{text "Command.thy"} is necessary for generating a log 
   file. This log file enables Isabelle to generate a keyword file containing 
-  the command \isacommand{foo}.\label{fig:commandtheory}}
+  the command \isacommand{foobar}.\label{fig:commandtheory}}
   \end{figure}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-  For 
-  our purposes it is sufficient to use the log files for the theories @{text "Pure"},
-  @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
-  containing the new \isacommand{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the 
-  installation of Isabelle. So log files for them are already available. If not, then they 
-  can be conveniently compiled using build-script from the distribution
+  For our purposes it is sufficient to use the log files for the theories
+  @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
+  the theory @{text "Command.thy"} containing the new
+  \isacommand{foobar}-command. @{text Pure} and @{text HOL} are usually
+  compiled during the installation of Isabelle. So log files for them should be
+  already available. If not, then they can be conveniently compiled using
+  build-script from the Isabelle distribution
 
   @{text [display] 
 "$ ./build -m \"Pure\"
@@ -632,23 +640,23 @@
   For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 
   with
 
-  @{text [display] "$ isabelle mkdir FooCommand"}
+  @{text [display] "$ isabelle mkdir FoobarCommand"}
 
   This creates a directory containing the files 
 
   @{text [display] 
 "./IsaMakefile
-./FooCommand/ROOT.ML
-./FooCommand/document
-./FooCommand/document/root.tex"}
+./FoobarCommand/ROOT.ML
+./FoobarCommand/document
+./FoobarCommand/document/root.tex"}
 
 
-  We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
+  We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
   and add the line 
 
   @{text [display] "use_thy \"Command\";"} 
   
-  to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing
+  to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
 
   @{text [display] "$ isabelle make"}
 
@@ -663,50 +671,139 @@
 
   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
  
-  In this directory are the files
+  on the Unix prompt. This directory should include the files
 
   @{text [display] 
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
-HOL-FooCommand.gz"} 
+HOL-FoobarCommand.gz"} 
 
-  They are used for creating the keyword files with the command
+  They are the ones we use for creating the keyword files. The corresponding  Unix command
+  is
 
 @{text [display]
-"$ isabelle keywords -k foo 
-       $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
+"$ isabelle keywords -k foobar 
+     $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
-  The result is the file @{text "isar-keywords-foo.el"}. This file needs to be 
-  copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
-  this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
+  The result is the file @{text "isar-keywords-foobar.el"}. It should contain the
+  string @{text "foobar"} twice (check for example that @{text [quotes] "grep foobar
+  isar-keywords-foobar.el"} returns something non-empty).  This keyword file
+  needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
+  Isabelle use this keyword file, we have to start it with the option @{text
+  "-k foobar"}, i.e.
 
-  @{text [display] "isabelle -k foo <a-theory-file>"}
+  @{text [display] "$ isabelle -k foobar a-theory-file"}
 
   If we now run the original code
+*}
 
-  @{ML [display]
-"let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+ML {*
+let
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+  OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end 
+*}
 
-  then we can make use of \isacommand{foo}! Similarly with any other new command. 
+text {*
+  then we can make use of \isacommand{foobar}! Similarly with any other new command. 
 
   In the example above, we built the theories on top of the HOL-logic. If you
-  target other logics, such as Nominal or ZF, then you need to change the
+  target other logics, such as Nominal or ZF, then you need to adapt the
   log files appropriately.
 
+  At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit 
+  by taking a proposition as argument and printing this proposition inside
+  the tracing buffer. 
+
+  The crucial part of a command is the function that determines
+  the behaviour of the command. In the code above we used the the 
+  @{text do_nothing}-function, which because of @{ML Scan.succeed} does not parse 
+  any argument, but immediately returns the simple toplevel function 
+  @{ML "Toplevel.theory I"}. We can replace this code by a function that first 
+  parses a proposition (using the parser @{ML OuterParse.prop}), then prints out 
+  the tracing information and finally does nothing. For this we can write
+*}
+
+ML {* 
+let
+  val trace_prop = 
+         OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
+  val kind = OuterKeyword.thy_decl
+in
+  OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
+end 
+*}
+
+text {*
+  Now we can type for example
+
+  @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
+  
+  and see the proposition in the tracing buffer.  
+
+  Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator
+  for the command.  This means that the command finishes as soon as the
+  arguments are processed. Examples of this kind of commands are
+  \isacommand{definition} and \isacommand{declare}.  In other cases, however,
+  commands are expected to parse some arguments, for example a proposition,
+  and then ``open up'' a proof in order to prove the proposition (think of
+  \isacommand{lemma}) or prove some other properties (for example in
+  \isacommand{function}). To achieve this behaviour we have to use the kind
+  indicator @{ML thy_goal in OuterKeyword}.
+
+  Below we change \isacommand{foobar} is such a way that an proposition as
+  argument and then start a proof in order to prove it. Therefore in Line 13
+  below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
+*}
+
+ML %linenumbers {*let
+  fun set_up_thm str ctxt =
+    let
+      val prop = Syntax.read_prop ctxt str
+    in
+      Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
+    end;
+  
+  val prove_prop = OuterParse.prop >>  
+      (fn str => Toplevel.print o 
+                    Toplevel.local_theory_to_proof NONE (set_up_thm str))
+  
+  val kind = OuterKeyword.thy_goal
+in
+  OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
+end 
+*}
+
+text {*
+  The function @{text set_up_thm} takes a string (the proposition) and a context.
+  The context is necessary in order to convert the string into a proper proposition
+  using the function @{ML Syntax.read_prop}. In Line 6 we use the function
+  @{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to
+  11 contain the parser for the proposition.
+
+  If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 
+  proof state:
+ 
+  @{ML_response_fake_both [display] "foobar \"True \<and> True\"" 
+"goal (1 subgoal):
+1. True \<and> True"}
+
+  and we can build the proof
+
+  @{text [display] "foobar \"True \<and> True\"
+apply(rule conjI)
+apply(rule TrueI)+
+done"} 
+  
+  (FIXME What does @{text "Toplevel.theory"}?)
+
   (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-  
 
 *}
 
-
-
-
 chapter {* Parsing *}
 
 text {*

--- a/CookBook/ROOT.ML	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/ROOT.ML	Wed Jan 14 16:46:07 2009 +0000
@@ -23,3 +23,4 @@
 
 use_thy "Solutions";
 use_thy "Readme";
+

--- a/CookBook/Recipes/Config.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/Config.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -75,16 +75,14 @@
   Config.get ctxt ival
 end" "4"}
 
-\begin{readmore}
+  \begin{readmore}
   For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
-\end{readmore}
+  \end{readmore}
 
-*}
-
-
-text {*
-
-  Note: Avoid to use references for this purpose!
+  There are many good reasons to control parameters in this way. One is
+  that it avoid global references, which cause many headaches with the
+  multithreaded execution of Isabelle.
+  
   *}
 
 end
\ No newline at end of file

--- a/CookBook/Recipes/NamedThms.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -22,13 +22,14 @@
   val name = "foo" 
   val description = "Rules for foo");
 *}
-(*<*)setup FooRules.setup(*>*)
 
 text {*
   and the command
+*}
 
-  @{text [display] "setup FooRules.setup"}
+setup {* FooRules.setup *}
 
+text {*
   This code declares a context data slot where the theorems are stored,
   an attribute @{text foo} (with the usual @{text add} and @{text del} options
   for adding and deleting theorems) and an internal ML interface to retrieve and 

--- a/CookBook/Recipes/StoringData.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -7,7 +7,7 @@
 
 text {*
   {\bf Problem:} 
-  Your tool needs to keep complex data.\smallskip
+  Your tool needs to manage data.\smallskip
 
   {\bf Solution:} This can be achieved using a generic data slot.\smallskip
 
@@ -16,15 +16,15 @@
 
   *}
 
-ML {* local
+ML {* 
+local
 
 structure Data = GenericDataFun
-(
-  type T = int Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge _ = Symtab.merge (K true)
-)
+ ( type T = int Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   fun merge _ = Symtab.merge (K true)
+ )
 
 in
 
@@ -36,7 +36,12 @@
 
 setup {* Context.theory_map (update "foo" 1) *}
 
-ML {* lookup (Context.Proof @{context}) "foo" *}
+text {*
+ 
+  @{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} 
+
+
+*}
 
 text {*
   alternatives: TheoryDataFun, ProofDataFun

--- a/CookBook/Recipes/TimeLimit.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -11,7 +11,7 @@
   {\bf Solution:} This can be achieved using the function 
   @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume the following infamous function:
+  Assume you defined the Ackermann function:
 
   *}
 
@@ -27,7 +27,7 @@
 
   @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
 
-  takes a bit of time to finish. To avoid this, the call can be encapsulated 
+  takes a bit of time before it finishes. To avoid this, the call can be encapsulated 
   in a time limit of five seconds. For this you have to write:
 
 @{ML_response [display]

Binary file cookbook.pdf has changed