--- a/CookBook/FirstSteps.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/FirstSteps.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -24,6 +24,8 @@
 
 section {* Including ML-Code *}
 
+
+
 text {*
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML} command. For example\smallskip
@@ -37,18 +39,8 @@
   Expressions inside \isacommand{ML} commands are immediately evaluated,
   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
   your Isabelle environment. The code inside the \isacommand{ML} command 
-  can also contain value and function bindings. However on such \isacommand{ML}
-  commands the undo operation behaves slightly counter-intuitive, because 
-  if you define\smallskip
- 
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
-\hspace{5mm}@{ML_text "val foo = true"}\isanewline
-\isacharverbatimclose\isanewline
-@{ML_text "> true"}\smallskip}
-
-  then Isabelle's undo operation has no effect on the definition of 
-  @{ML_text "foo"}. Note that from now on we will drop the 
+  can also contain value and function bindings, and even those can be
+  undone when the proof script is retracted. From now on we will drop the 
   \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
   we show code and its response.
 
@@ -78,7 +70,7 @@
 
   @{ML [display] "warning \"any string\""}
 
-  will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle.
+  will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle.
   If you develop under PolyML, then there is a convenient, though again 
   ``quick-and-dirty'', method for converting values into strings, 
   for example: 
@@ -101,7 +93,7 @@
   amounts of trace output. This rediretion can be achieved using the code
 *}
 
-ML {*
+ML{* 
 val strip_specials =
 let
   fun strip ("\^A" :: _ :: cs) = strip cs
@@ -113,7 +105,7 @@
  Output.tracing_fn := (fn s =>
     (TextIO.output (stream, (strip_specials s));
      TextIO.output (stream, "\n");
-     TextIO.flushOut stream));
+     TextIO.flushOut stream)); 
 *}
 
 text {*
@@ -163,8 +155,8 @@
   @{ML [display] "@{thm allI}"}
   @{ML [display] "@{simpset}"}
 
-  While antiquotations have many uses, they were introduced to avoid explicit
-  bindings for theorems such as
+  While antiquotations have many applications, they were originally introduced to 
+  avoid explicit bindings for theorems such as
 *}
 
 ML {*
@@ -172,14 +164,12 @@
 *}
 
 text {*
-  These bindings were difficult to maintain and also could be overwritten
-  by bindings introduced by the user. This had the potential to break
-  definitional packages. This additional layer of maintenance complexity
-  can be avoided by using antiquotations, since they are ``linked'' statically
-  at compile time.  In the course of this introduction, we will learn more about 
-  these antiquotations: they greatly simplify Isabelle programming since one
-  can directly access all kinds of logical elements from ML.
-
+  These bindings were difficult to maintain and also could be accidentally overwritten
+  by the user. This usually broke definitional packages. Antiquotations solve this
+  problem, since they are ``linked'' statically at compile time.  In the course of this 
+  introduction, we will learn more about these antiquotations: they greatly simplify 
+  Isabelle programming since one can directly access all kinds of logical elements 
+  from ML.
 *}
 
 section {* Terms and Types *}
@@ -208,10 +198,8 @@
 
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user level, because the layers of
-  parsing/type checking/pretty printing can be quite elaborate. 
-*}
+  parsing/type-checking/pretty printing can be quite elaborate. 
 
-text {*
   \begin{exercise}
   Look at the internal term representation of the following terms, and
   find out why they are represented like this.
@@ -246,24 +234,14 @@
   which does not. 
 
   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
-  
-  *}
-
-
-text {*
 
   @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
-  (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
-  internal representation. Is there a reason for this, that needs to be explained 
-  here?)
-
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
   definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
   \end{readmore}
-
-  *}
+*}
 
 
 section {* Constructing Terms and Types Manually *} 
@@ -271,7 +249,7 @@
 text {*
 
   While antiquotations are very convenient for constructing terms and types, 
-  they can only construct fixed terms. Unfortunately, one often needs to construct them 
+  they can only construct fixed terms. Unfortunately, one often needs to construct terms
   dynamically. For example, a function that returns the implication 
   @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
   as arguments can only be written as
@@ -289,7 +267,8 @@
 text {*
 
   The reason is that one cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example the following does not work.
+  @{term "tau"} into an antiquotation. For example the following does not work as
+  expected.
 *}
 
 ML {*
@@ -350,6 +329,8 @@
 
 section {* Type Checking *}
 
+ML {* cterm_of @{theory} @{term "a + b = c"} *}
+
 text {* 
   
   We can freely construct and manipulate terms, since they are just
@@ -364,11 +345,15 @@
 
   Type checking is always relative to a theory context. For now we can use
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
-  For example we can write:
+  For example we can write
+
+  @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+
+  or use the antiquotation
 
   @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 
-  and 
+  A slightly more elaborate example is
 
 @{ML_response_fake [display] 
 "let

--- a/CookBook/Parsing.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Parsing.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -15,7 +15,7 @@
   Isabelle uses a rather general and sophisticated algorithm due to Earley, which 
   is driven by priority grammars. Parsers for outer syntax are built up by functional
   parsing combinators. These combinators are a well-established technique for parsing, 
-  which has, for example, been described in Paulson's classic book \cite{paulson-ml2}.
+  which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
   Isabelle developers are usually concerned with writing these outer syntax parsers, 
   either for new definitional packages or for calling tactics with specific arguments. 
 
@@ -110,11 +110,11 @@
   
 @{ML_response [display]
 "let 
-  val just_h = ($$ \"h\") |-- ($$ \"e\") 
-  val just_e = ($$ \"h\") --| ($$ \"e\") 
+  val just_e = ($$ \"h\") |-- ($$ \"e\") 
+  val just_h = ($$ \"h\") --| ($$ \"e\") 
   val input = (explode \"hello\")  
 in 
-  (just_h input, just_e input)
+  (just_e input, just_h input)
 end"
   "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"}
 
@@ -182,7 +182,7 @@
 *}
 
 ML {* 
-  fun p_followed_by_q p q r =
+fun p_followed_by_q p q r =
   let 
      val err = (fn _ => p ^ " is not followed by " ^ q)
   in
@@ -258,7 +258,9 @@
 
   The structure @{ML_struct OuterLex} defines several kinds of token (for example 
   @{ML "OuterLex.Ident"} for identifiers, @{ML "OuterLex.Keyword"} for keywords and
-  @{ML "OuterLex.Command"} for commands).
+  @{ML "OuterLex.Command"} for commands). Some parsers take into account the 
+  kind of token.
+  
   We can generate a token list using the function @{ML "OuterSyntax.scan"}, which we give
   below @{ML "Position.none"} as argument since, at the moment, we are not interested in
   generating precise error messages. The following\footnote{There is something funny 
@@ -269,7 +271,7 @@
  OuterLex.Token (\<dots>,(OuterLex.Space, \" \"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Ident, \"world\"),\<dots>)]"}
 
-  produces three token where the first and the last are identifiers, since 
+  produces three tokens where the first and the last are identifiers, since 
   @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match 
   any other category. The second indicates a space. If we parse
 
@@ -278,7 +280,18 @@
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"|\"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"for\"),\<dots>)]"}
 
-  we obtain a list of command/keyword token.
+  we obtain a list of command and keyword tokens.
+  If you want to see which keywords and commands are currently known, use
+  the following (you might have to adjust the @{ML print_depth} in order to
+  see the complete list):
+
+@{ML_response_fake [display] 
+"let 
+  val (keywords, commands) = OuterKeyword.get_lexicons ()
+in 
+  (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
+end" 
+"([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}
 
   Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
  
@@ -314,7 +327,10 @@
 end" 
 "([\"in\",\"in\",\"in\"],[\<dots>])"}
 
- @{ML_open "OuterParse.enum1"} works similarly, except that the list must be non-empty.
+  Note that we had to add a @{ML_text [quotes] "\\n"} at the end of the parsed
+  string, otherwise the parser would have consumed all tokens and then failed with
+  the exception @{ML_text "FAIL"}. @{ML "OuterParse.enum1"} works similarly, 
+  except that the parsed list must be non-empty.
 
 *}
 
@@ -331,7 +347,7 @@
 
 *}
 
-text {* FIXME funny output for a proposition *}
+text {* (FIXME funny output for a proposition) *}
 
 
 
@@ -562,21 +578,36 @@
 
 *}
 
-text {*
-  FIXME
+
+
 
-  @{text "
-  begin{verbatim}
-  type token = T.token ;
-  val toks : token list = OuterSyntax.scan ``theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }'' ;
+ML {*
+  val toks = OuterSyntax.scan Position.none
+   "theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ;
+*}
+
+ML {*
   print_depth 20 ;
-  List.map T.text_of toks ;
-  val proper_toks = List.filter T.is_proper toks ;
-  List.map T.kind_of proper_toks ;
-  List.map T.unparse proper_toks ;
-  List.map T.val_of proper_toks ;
-  end{verbatim}"}
+*}
+
+ML {*
+  map OuterLex.text_of toks ;
+*}
+
+ML {*
+  val proper_toks = filter OuterLex.is_proper toks ;
+*}  
 
+ML {*
+  map OuterLex.kind_of proper_toks 
+*}
+
+ML {*
+  map OuterLex.unparse proper_toks ;
+*}
+
+ML {*
+  OuterLex.stopper
 *}
 
 text {*

--- a/CookBook/Readme.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Readme.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -8,7 +8,7 @@
 
   \begin{itemize}
   \item You can make references to other Isabelle manuals using the 
-  reference names from those manuals. For this the following
+  reference names from those manuals. To do this the following
   four latex commands are defined:
   
   \begin{center}

--- a/CookBook/Recipes/Antiquotes.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -1,24 +1,31 @@
 
 theory Antiquotes
-imports Main
+imports "../Base"
 begin
 
 
-section {* Two Document Antiquotations *}
+section {* Useful Document Antiquotations *}
 
 text {*
+  {\bf Problem:} 
+  How to keep ML-code included in a document in sync with the actual code.\smallskip
 
-  For writing documents using Isabelle it is often uesful to use
-  document antiquotations. Below we give the code for such an 
-  antiquotation that typesets ML-code and also checks whether
-  the code is actually correct. In this way one can achieve that the
-  document is always in sync with code.
+  {\bf Solution:} This can be achieved using document antiquotations.\smallskip
+
+  Document antiquotations are a convenient method for type-setting consitently 
+  a group of items in a document. They can also be used for sophisticated
+  \LaTeX hacking.  
 
-  Below we introduce the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which
-  takes a piece of code as argument. We will check this code by sending 
-  the ML-expression @{text "val _ = \<dots>"} to the ML-compiler (i.e.~the 
-  function @{ML "ML_Context.eval_in"}). The code for this antiquotation
-  is as follows:
+  Below we give the code for two such 
+  antiquotations that can be used to typeset ML-code and also to check whether
+  the code is actually compiles. In this way one can relatively easily 
+  keep documents in sync with code.
+
+  We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which
+  takes a piece of code as argument. This code is checked by sending 
+  the ML-expression @{text "val _ = \<dots>"} containing the given code to the 
+  ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code 
+  for this antiquotation is as follows:
 *}
 
 ML {*
@@ -26,7 +33,8 @@
 
 fun output_ml ml src ctxt txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
-  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
+                                            (space_explode "\n" txt))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))]
@@ -37,21 +45,25 @@
   Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the
   code is approved by the compiler, the output function 
   @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"}
-  pretty prints the code. There are a number of options that are observed
-  when printing the code (for example @{text "[display]"}; for more information
-  about the options see \rsccite{sec:antiq}).
+  pretty prints the code. This function expects that the code is a list of strings
+  according to the line breaks (therefore the 
+  @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list).
+  There are a number of options that are observed by @{ML ThyOutput.output_list}
+  when printing the code (for example @{text "[display]"} and @{text "[source]"}; 
+  for more information about these options see \rsccite{sec:antiq}).
 
-  Since we
-  used the argument @{ML "Position.none"}, the compiler cannot give specific 
+  Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
   information about the line number where an error might have occurred. We 
   can improve this code slightly by writing 
 
+  The second 
 *}
 
 ML {*
 fun output_ml ml src ctxt (txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
-  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
+                                            (space_explode "\n" txt))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args 
@@ -59,16 +71,12 @@
 *}
 
 text {*
-  where the antiquotation can also handle position information.
-
   (FIXME: say something about OuterParse.position)
-
 *}
 
 ML {*
-
 fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
+  let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
   in
     "val " ^ pat' ^ " = " ^ rhs
   end;
@@ -80,7 +88,6 @@
   (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
-
 *}
 
 

--- a/CookBook/Recipes/NamedThms.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -9,46 +9,53 @@
   {\bf Problem:} 
   Your tool @{text foo} works with special rules, called @{text foo}-rules.
   Users should be able to declare @{text foo}-rules in the theory,
-  which are then used by some method.\smallskip
+  which are then used in a method.\smallskip
 
-  {\bf Solution:} This can be achieved using 
+  {\bf Solution:} This can be achieved using named theorem lists.\smallskip
+
+  Named theorem lists can be set up using the code
 
   *}
+
 ML {*
-  structure FooRules = NamedThmsFun(
-    val name = "foo" 
-    val description = "Rules for foo"
-  );
+structure FooRules = NamedThmsFun (
+  val name = "foo" 
+  val description = "Rules for foo");
 *}
-
-setup FooRules.setup
+(*<*)setup FooRules.setup(*>*)
 
 text {*
+  and the command
+
+  @{ML_text [display] "setup FooRules.setup"}
+
   This code declares a context data slot where the theorems are stored,
   an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options
   to adding and deleting theorems) and an internal ML interface to retrieve and 
   modify the theorems.
 
   Furthermore, the facts are made available on the user level under the dynamic 
-  fact name @{text foo}. For example:
+  fact name @{text foo}. For example we can declare two lemmas to be of the kind
+  @{ML_text foo}:
 *}
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 
+text {* undeclare them: *}
+
 declare rule1[foo del]
 
+text {* and query them: *}
+
 thm foo
 
 text {* 
   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
   using
-*}
 
-ML {* FooRules.get @{context} *}
+  @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"}
 
-
-text {* 
   \begin{readmore}
   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
   \end{readmore}

--- a/CookBook/Solutions.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Solutions.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -7,20 +7,20 @@
 text {* \solution{fun:revsum} *}
 
 ML {* 
-  fun rev_sum t =
-  let
-   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
-     | dest_sum u = [u]
-   in
-     foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
-   end;
+fun rev_sum t =
+let
+ fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
+   | dest_sum u = [u]
+ in
+   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
+ end;
 *}
 
 text {* \solution{fun:makesum} *}
 
 ML {*
-  fun make_sum t1 t2 =
-      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
+fun make_sum t1 t2 =
+    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
 *}
 
 end
\ No newline at end of file

--- a/CookBook/document/root.tex	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/document/root.tex	Thu Oct 30 13:36:51 2008 +0100
@@ -9,8 +9,16 @@
 \usepackage{rail}
 \usepackage{url}
 \usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
+\usepackage{pdfsetup}
 
-% Cross references to other manuals:
+\urlstyle{rm}
+\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
+\renewcommand{\isastyleminor}{\tt\slshape}%
+\renewcommand{\isastyle}{\small\tt\slshape}%
+\isadroptag{theory}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% For cross references to the other manuals:
 \usepackage{xr}
 \externaldocument[I-]{implementation}
 \newcommand{\impref}[1]{\ref{I-#1}}
@@ -21,41 +29,54 @@
 \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
 \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
 
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
-\renewcommand{\isastyleminor}{\tt\slshape}%
-\renewcommand{\isastyle}{\small\tt\slshape}%
-\isadroptag{theory}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % sane default for proof documents
 \parindent 0pt\parskip 0.6ex
 
-% for comments on the margin
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% to work around a problem with \isanewline
+\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% FIXME: WHAT DOES THIS DO?
+\renewenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\small\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for exercises, comments and readmores
+\newtheorem{exercise}{Exercise}[section]
+\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
+
 \newcommand{\readmoremarginpar}[1]%
 {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
 
 \newenvironment{readmore}%
 {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
 
-% to work around a problem with \isanewline
-\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
-
-\renewenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\small\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-% for exercises and comments
-\newtheorem{exercise}{Exercise}[section]
-\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% FIXME: THIS SHOULD NOT BE USED ANYMORE
 % a table environment with proper indentation
-\newenvironment{mytable}{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}{\end{tabular}\end{trivlist}}
+\newenvironment{mytable}
+{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}
+{\end{tabular}\end{trivlist}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \hyphenation{Isabelle}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% this hack is for getting rid of the ML {* ... *} 
+% scaffolding around function definitions
+\newenvironment{vanishML}{%
+\renewcommand{\isacommand}[1]{}%
+\renewcommand{\isacharverbatimopen}{}%
+\renewcommand{\isacharverbatimclose}{}%
+\hspace{-1.5mm}\mbox{}}{}
+
+\renewcommand{\isatagML}{\begin{vanishML}}
+\renewcommand{\endisatagML}{\end{vanishML}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \begin{document}
 
 \title{\mbox{}\\[-10ex]
@@ -71,7 +92,6 @@
 
 \tableofcontents
 
-
 % generated text of all theories
 \input{session}
 

Binary file cookbook.pdf has changed