--- a/CookBook/FirstSteps.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -30,11 +30,10 @@
 
 \begin{isabelle}
 \begin{graybox}
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
+\isacommand{ML}~@{text "\<verbopen>"}\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
-\isacharverbatimclose\isanewline
-@{text "> 7"}\smallskip}
+@{text "\<verbclose>"}\isanewline
+@{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
 
@@ -43,7 +42,7 @@
   your Isabelle environment. The code inside the \isacommand{ML}-command 
   can also contain value and function bindings, and even those can be
   undone when the proof script is retracted. As mentioned earlier, we will  
-  drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} 
   whenever we show code.
 
   Once a portion of code is relatively stable, one usually wants to 

--- a/CookBook/Intro.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Intro.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -71,18 +71,16 @@
 
   \begin{isabelle}
   \begin{graybox}
-  \isa{\isacommand{ML}
-  \isacharverbatimopen\isanewline
+  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
   \hspace{5mm}@{ML "3 + 4"}\isanewline
-  \isacharverbatimclose}
+  @{text "\<verbclose>"}
   \end{graybox}
   \end{isabelle}
   
   This corresponds to how code can be processed inside the interactive
   environment of Isabelle. It is therefore easy to experiment with the code
   (which by the way is highly recommended). However, for better readability we
-  will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
-  \isacharverbatimclose} and just write
+  will drop the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write
 
 
   @{ML [display,gray] "3 + 4"}

--- a/CookBook/Parsing.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -597,7 +597,7 @@
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
-  \isacommand{ML}~\isa{\isacharverbatimopen}\\
+  \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
   val do_nothing = Scan.succeed (Toplevel.theory I)
@@ -605,7 +605,7 @@
 in
   OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
-  \isa{\isacharverbatimclose}\\
+  @{text "\<verbclose>"}\\
   \isacommand{end}
   \end{graybox}
   \caption{\small The file @{text "Command.thy"} is necessary for generating a log 

--- a/CookBook/Readme.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Readme.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -143,12 +143,12 @@
 
 
   \item Functions and value bindings cannot be defined inside antiquotations; they need
-  to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
+  to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
   the Cookbook, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}
   for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
 
   \end{itemize}

--- a/CookBook/document/root.tex	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/document/root.tex	Tue Jan 27 21:22:27 2009 +0000
@@ -85,6 +85,12 @@
 \renewenvironment{isabelle}
 {\begin{trivlist}\begin{isabellebody}\small\item\relax}
 {\end{isabellebody}\end{trivlist}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for {*  *} in antiquotations
+\newcommand{\isasymverbopen}{\isacharverbatimopen}
+\newcommand{\isasymverbclose}{\isacharverbatimclose}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 

Binary file cookbook.pdf has changed