diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Readme.thy
--- a/ProgTutorial/Readme.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Readme.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
 imports Base
 begin
 
-chapter {* Comments for Authors *}
+chapter \<open>Comments for Authors\<close>
 
-text {*
+text \<open>
 
   \begin{itemize}
   \item This tutorial can be compiled on the command-line with:
@@ -22,12 +22,12 @@
   \begin{center}
   \begin{tabular}{l|c|c}
    & Chapters & Sections\\\hline
-  Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\
-  Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\
+  Implementation Manual & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\
+  Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\
   \end{tabular}
   \end{center}
 
-  So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 
+  So \<open>\ichcite{ch:logic}\<close> yields a reference for the chapter about logic 
   in the implementation manual, namely \ichcite{ch:logic}.
 
   \item There are various document antiquotations defined for the 
@@ -39,33 +39,32 @@
   The following antiquotations are defined:
 
   \begin{itemize}
-  \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used
+  \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used
   for displaying any ML-ex\-pression, because the antiquotation checks whether
-  the expression is valid ML-code. The @{text "for"}- and @{text
-  "in"}-arguments are optional. The former is used for evaluating open
+  the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open
   expressions by giving a list of free variables. The latter is used to
   indicate in which structure or structures the ML-expression should be
   evaluated. Examples are:
   
   \begin{center}\small
   \begin{tabular}{lll}
-  @{text "@{ML \"1 + 3\"}"}         &                 & @{ML "1 + 3"}\\
-  @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\
-  @{text "@{ML Ident in OuterLex}"} &                 & @{ML Ident in OuterLex}\\
+  \<open>@{ML "1 + 3"}\<close>         &                 & @{ML "1 + 3"}\\
+  \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\
+  \<open>@{ML Ident in OuterLex}\<close> &                 & @{ML Ident in OuterLex}\\
   \end{tabular}
   \end{center}
 
-  \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to
+  \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> should be used to
   display ML-expressions and their response.  The first expression is checked
-  like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern
+  like in the antiquotation \<open>@{ML "expr"}\<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
   first expression will be checked against this pattern. Examples are:
 
   \begin{center}\small
   \begin{tabular}{l}
-  @{text "@{ML_response \"1+2\" \"3\"}"}\\
-  @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}
+  \<open>@{ML_response "1+2" "3"}\<close>\\
+  \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close>
   \end{tabular}
   \end{center}
 
@@ -82,18 +81,18 @@
   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$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just
-  like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,
+  \item[$\bullet$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just
+  like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> above,
   except that the result-specification is not checked. Use this antiquotation
   when the result cannot be constructed or the code generates an
   exception. Examples are:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\
-                               & @{text "\"a + b = c\"}"}\smallskip\\ 
-  @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ 
-                               & @{text "\"Exception FAIL raised\"}"}
+  \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+                               & \<open>"a + b = c"}\<close>\smallskip\\ 
+  \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ 
+                               & \<open>"Exception FAIL raised"}\<close>
   \end{tabular}
   \end{center}
 
@@ -109,50 +108,50 @@
   This output mimics to some extend what the user sees when running the
   code.
 
-  \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be
+  \item[$\bullet$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> can be
   used to show erroneous code. Neither the code nor the response will be
   checked. An example is:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\
-                                    & @{text "\"Type unification failed \<dots>\"}"}
+  \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+                                    & \<open>"Type unification failed \<dots>"}\<close>
   \end{tabular}
   \end{center}
 
-  \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
+  \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when
   referring to a file. It checks whether the file exists.  An example
   is 
 
   @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
   \end{itemize}
 
-  The listed antiquotations honour options including @{text "[display]"} and 
-  @{text "[quotes]"}. For example
+  The listed antiquotations honour options including \<open>[display]\<close> and 
+  \<open>[quotes]\<close>. For example
 
   \begin{center}\small
-  @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
+  \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
   \end{center}
 
   whereas
   
   \begin{center}\small
-  @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
+  \<open>@{ML "\"foo\" ^ \"bar\""}\<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}~@{text "\<verbopen> \<dots> \<verbclose>"}
+  to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
   the tutorial, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}
-  for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The
+  \isacommand{ML} \isa{\%linenos}~\<open>\<verbopen> \<dots> \<verbclose>\<close>
+  for ML-code or \isacommand{lemma} \isa{\%linenos} \<open>...\<close> for proofs. The
   tag is \isa{\%linenosgray} when the numbered text should be gray. 
 
   \end{itemize}
 
-*}
+\<close>