--- a/ProgTutorial/Readme.thy	Fri May 17 10:50:53 2019 +0200
+++ b/ProgTutorial/Readme.thy	Fri May 17 11:21:09 2019 +0200
@@ -9,7 +9,7 @@
   \begin{itemize}
   \item This tutorial can be compiled on the command-line with:
 
-  @{text [display] "$ isabelle make"}
+  @{text [display] "$ isabelle build -c -v -d . Cookbook"}
 
   You very likely need a recent snapshot of Isabelle in order to compile
   the tutorial. Some parts of the tutorial also rely on compilation with
@@ -58,13 +58,14 @@
   display ML-expressions and their response.  The first expression is checked
   like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern
   that specifies the result the first expression produces. This pattern can
-  contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
+  contain @{text [quotes] "_"} (which will be printed as @{text [quotes] "\<dots>"}) 
+  for parts that you like to omit. The response of the
   first expression will be checked against this pattern. Examples are:
 
   \begin{center}\small
   \begin{tabular}{l}
   \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\
-  \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close>
+  \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}\<close>
   \end{tabular}
   \end{center}
 
@@ -81,7 +82,7 @@
   constructed: it does not work when the code produces an exception or returns 
   an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
-  \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just
+  \item[$\bullet$] \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> works just
   like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above,
   except that the result-specification is not checked. Use this antiquotation
   when the result cannot be constructed or the code generates an
@@ -89,10 +90,10 @@
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\
-                               & \<open>"a + b = c"}\<close>\smallskip\\ 
-  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\ 
-                               & \<open>"Exception FAIL raised"}\<close>
+  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>}\<close>\\
+                               & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ 
+  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ 
+                               & \<open>\<open>Exception FAIL raised\<close>}\<close>
   \end{tabular}
   \end{center}
 
@@ -108,7 +109,7 @@
   This output mimics to some extend what the user sees when running the
   code.
 
-  \item[$\bullet$] \<open>@{ML_matchresult_fake_both "expr" "pat"}\<close> can be
+  \item[$\bullet$] \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close> can be
   used to show erroneous code. Neither the code nor the response will be
   checked. An example is:
 
@@ -119,6 +120,24 @@
   \end{tabular}
   \end{center}
 
+  \item[$\bullet$] \<open>@{ML_response \<open>expr\<close>}\<close> can be
+  used to show the expression and the corresponding output. An example is:
+
+  \begin{center}\small
+  \begin{tabular}{ll}
+  \<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close>
+  \end{tabular}
+  \end{center}
+
+ which produce respectively
+
+  \begin{center}\small
+  \begin{tabular}{p{3cm}p{3cm}}
+  @{ML_response \<open>1 upto 10\<close>}
+  \end{tabular}
+  \end{center}
+ 
+
   \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when
   referring to a file. It checks whether the file exists.  An example
   is 
@@ -127,17 +146,8 @@
   \end{itemize}
 
   The listed antiquotations honour options including \<open>[display]\<close> and 
-  \<open>[quotes]\<close>. For example
-
-  \begin{center}\small
-  \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
-  \end{center}
+  \<open>[gray]\<close>. For example
 
-  whereas
-  
-  \begin{center}\small
-  \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close>
-  \end{center}
   
   \item Functions and value bindings cannot be defined inside antiquotations; they need
   to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>

--- a/ROOT	Fri May 17 10:50:53 2019 +0200
+++ b/ROOT	Fri May 17 11:21:09 2019 +0200
@@ -25,6 +25,7 @@
     "Recipes/Sat"
     "Recipes/USTypes"
     "Solutions"
+    "Readme"
   document_files
     "root.bib"
     "root.tex"