diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -2,9 +2,9 @@
 theory Documents imports Main begin
 (*>*)
 
-section {* Concrete Syntax \label{sec:concrete-syntax} *}
+section \<open>Concrete Syntax \label{sec:concrete-syntax}\<close>
 
-text {*
+text \<open>
   The core concept of Isabelle's framework for concrete syntax is that
   of \bfindex{mixfix annotations}.  Associated with any kind of
   constant declaration, mixfixes affect both the grammar productions
@@ -19,12 +19,12 @@
 
   Below we introduce a few simple syntax declaration
   forms that already cover many common situations fairly well.
-*}
+\<close>
 
 
-subsection {* Infix Annotations *}
+subsection \<open>Infix Annotations\<close>
 
-text {*
+text \<open>
   Syntax annotations may be included wherever constants are declared,
   such as \isacommand{definition} and \isacommand{primrec} --- and also
   \isacommand{datatype}, which declares constructor operations.
@@ -35,12 +35,12 @@
   Infix declarations\index{infix annotations} provide a useful special
   case of mixfixes.  The following example of the exclusive-or
   operation on boolean values illustrates typical infix declarations.
-*}
+\<close>
 
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
-text {*
+text \<open>
   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
   same expression internally.  Any curried function with at least two
   arguments may be given infix syntax.  For partial applications with
@@ -75,12 +75,12 @@
   below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
   above 50.  User syntax should strive to coexist with common HOL
   forms, or use the mostly unused range 100--900.
-*}
+\<close>
 
 
-subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
+subsection \<open>Mathematical Symbols \label{sec:syntax-symbols}\<close>
 
-text {*
+text \<open>
   Concrete syntax based on ASCII characters has inherent limitations.
   Mathematical notation demands a larger repertoire of glyphs.
   Several standards of extended character sets have been proposed over
@@ -133,39 +133,39 @@
 
   Replacing our previous definition of @{text xor} by the
   following specifies an Isabelle symbol for the new operator:
-*}
+\<close>
 
 (*<*)
 hide_const xor
-setup {* Sign.add_path "version1" *}
+setup \<open>Sign.add_path "version1"\<close>
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 (*<*)
-setup {* Sign.local_path *}
+setup \<open>Sign.local_path\<close>
 (*>*)
 
-text {*
+text \<open>
   It is possible to provide alternative syntax forms
   through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of @{text xor}:
-*}
+\<close>
 
 (*<*)
 hide_const xor
-setup {* Sign.add_path "version2" *}
+setup \<open>Sign.add_path "version2"\<close>
 (*>*)
 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
 
 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
 (*<*)
-setup {* Sign.local_path *}
+setup \<open>Sign.local_path\<close>
 (*>*)
 
-text {*\noindent
+text \<open>\noindent
 The \commdx{notation} command associates a mixfix
 annotation with a known constant.  The print mode specification,
 here @{text "(xsymbols)"}, is optional.
@@ -174,17 +174,17 @@
 output uses the nicer syntax of $xsymbols$ whenever that print mode is
 active.  Such an arrangement is particularly useful for interactive
 development, where users may type ASCII text and see mathematical
-symbols displayed during proofs.  *}
+symbols displayed during proofs.\<close>
 
 
-subsection {* Prefix Annotations *}
+subsection \<open>Prefix Annotations\<close>
 
-text {*
+text \<open>
   Prefix syntax annotations\index{prefix annotation} are another form
   of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
   priorities --- just some literal syntax.  The following example
   associates common symbols with the constructors of a datatype.
-*}
+\<close>
 
 datatype currency =
     Euro nat    ("\<euro>")
@@ -192,7 +192,7 @@
   | Yen nat     ("\<yen>")
   | Dollar nat  ("$")
 
-text {*
+text \<open>
   \noindent Here the mixfix annotations on the rightmost column happen
   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
@@ -204,12 +204,12 @@
   Commission.
 
   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
-*}
+\<close>
 
 
-subsection {* Abbreviations \label{sec:abbreviations} *}
+subsection \<open>Abbreviations \label{sec:abbreviations}\<close>
 
-text{* Mixfix syntax annotations merely decorate particular constant
+text\<open>Mixfix syntax annotations merely decorate particular constant
 application forms with concrete syntax, for instance replacing
 @{text "xor A B"} by @{text "A \<oplus> B"}.  Occasionally, the relationship
 between some piece of notation and its internal form is more
@@ -223,12 +223,12 @@
 A typical use of abbreviations is to introduce relational notation for
 membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by
 @{text "x \<approx> y"}. We assume that a constant @{text sim } of type
-@{typ"('a \<times> 'a) set"} has been introduced at this point. *}
+@{typ"('a \<times> 'a) set"} has been introduced at this point.\<close>
 (*<*)consts sim :: "('a \<times> 'a) set"(*>*)
 abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)
 where "x \<approx> y  \<equiv>  (x, y) \<in> sim"
 
-text {* \noindent The given meta-equality is used as a rewrite rule
+text \<open>\noindent The given meta-equality is used as a rewrite rule
 after parsing (replacing \mbox{@{prop"x \<approx> y"}} by @{text"(x,y) \<in>
 sim"}) and before printing (turning @{text"(x,y) \<in> sim"} back into
 \mbox{@{prop"x \<approx> y"}}). The name of the dummy constant @{text "sim2"}
@@ -238,14 +238,14 @@
 provide variant versions of fundamental relational expressions, such
 as @{text \<noteq>} for negated equalities.  The following declaration
 stems from Isabelle/HOL itself:
-*}
+\<close>
 
 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
 
 notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
 
-text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
+text \<open>\noindent The notation @{text \<noteq>} is introduced separately to restrict it
 to the \emph{xsymbols} mode.
 
 Abbreviations are appropriate when the defined concept is a
@@ -257,12 +257,12 @@
 Abbreviations are a simplified form of the general concept of
 \emph{syntax translations}; even heavier transformations may be
 written in ML @{cite "isabelle-isar-ref"}.
-*}
+\<close>
 
 
-section {* Document Preparation \label{sec:document-preparation} *}
+section \<open>Document Preparation \label{sec:document-preparation}\<close>
 
-text {*
+text \<open>
   Isabelle/Isar is centered around the concept of \bfindex{formal
   proof documents}\index{documents|bold}.  The outcome of a formal
   development effort is meant to be a human-readable record, presented
@@ -279,27 +279,27 @@
 
   Here is an example to illustrate the idea of Isabelle document
   preparation.
-*}
+\<close>
 
-text_raw {* \begin{quotation} *}
+text_raw \<open>\begin{quotation}\<close>
 
-text {*
+text \<open>
   The following datatype definition of @{text "'a bintree"} models
   binary trees with nodes being decorated by elements of type @{typ
   'a}.
-*}
+\<close>
 
 datatype 'a bintree =
      Leaf | Branch 'a  "'a bintree"  "'a bintree"
 
-text {*
+text \<open>
   \noindent The datatype induction rule generated here is of the form
   @{thm [indent = 1, display] bintree.induct [no_vars]}
-*}
+\<close>
 
-text_raw {* \end{quotation} *}
+text_raw \<open>\end{quotation}\<close>
 
-text {*
+text \<open>
   \noindent The above document output has been produced as follows:
 
   \begin{ttbox}
@@ -324,12 +324,12 @@
   to formal entities by means of ``antiquotations'' (such as
   \texttt{\at}\verb,{text "'a bintree"}, or
   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
-*}
+\<close>
 
 
-subsection {* Isabelle Sessions *}
+subsection \<open>Isabelle Sessions\<close>
 
-text {*
+text \<open>
   In contrast to the highly interactive mode of Isabelle/Isar theory
   development, the document preparation stage essentially works in
   batch-mode.  An Isabelle \bfindex{session} consists of a collection
@@ -412,12 +412,12 @@
   Isabelle batch session leaves the generated sources in their target
   location, identified by the accompanying error message.  This lets
   you trace {\LaTeX} problems with the generated files at hand.
-*}
+\<close>
 
 
-subsection {* Structure Markup *}
+subsection \<open>Structure Markup\<close>
 
-text {*
+text \<open>
   The large-scale structure of Isabelle documents follows existing
   {\LaTeX} conventions, with chapters, sections, subsubsections etc.
   The Isar language includes separate \bfindex{markup commands}, which
@@ -460,12 +460,12 @@
 
   end
   \end{ttbox}
-*}
+\<close>
 
 
-subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
+subsection \<open>Formal Comments and Antiquotations \label{sec:doc-prep-text}\<close>
 
-text {*
+text \<open>
   Isabelle \bfindex{source comments}, which are of the form
   \verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like
   white space and do not really contribute to the content.  They
@@ -481,14 +481,14 @@
   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
   marginal comments may be given at the same time.  Here is a simple
   example:
-*}
+\<close>
 
 lemma "A --> A"
-  -- "a triviality of propositional logic"
-  -- "(should not really bother)"
-  by (rule impI) -- "implicit assumption step involved here"
+  \<comment> "a triviality of propositional logic"
+  \<comment> "(should not really bother)"
+  by (rule impI) \<comment> "implicit assumption step involved here"
 
-text {*
+text \<open>
   \noindent The above output has been produced as follows:
 
 \begin{verbatim}
@@ -593,12 +593,12 @@
   document very easily, independently of the term language of
   Isabelle.  Manual {\LaTeX} code would leave more control over the
   typesetting, but is also slightly more tedious.
-*}
+\<close>
 
 
-subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
+subsection \<open>Interpretation of Symbols \label{sec:doc-prep-symbols}\<close>
 
-text {*
+text \<open>
   As has been pointed out before (\S\ref{sec:syntax-symbols}),
   Isabelle symbols are the smallest syntactic entities --- a
   straightforward generalization of ASCII characters.  While Isabelle
@@ -640,12 +640,12 @@
   quotes are not printed at all.  The resulting quality of typesetting
   is quite good, so this should be the default style for work that
   gets distributed to a broader audience.
-*}
+\<close>
 
 
-subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
+subsection \<open>Suppressing Output \label{sec:doc-prep-suppress}\<close>
 
-text {*
+text \<open>
   By default, Isabelle's document system generates a {\LaTeX} file for
   each theory that gets loaded while running the session.  The
   generated \texttt{session.tex} will include all of these in order of
@@ -683,11 +683,11 @@
   commands involving ML code).  Users may add their own tags using the
   \verb,%,\emph{tag} notation right after a command name.  In the
   subsequent example we hide a particularly irrelevant proof:
-*}
+\<close>
 
 lemma "x = x" by %invisible (simp)
 
-text {*
+text \<open>
   The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
   Tags observe the structure of proofs; adjacent commands with the
   same tag are joined into a single region.  The Isabelle document
@@ -705,12 +705,12 @@
   of the theory, of course.  For example, we may hide parts of a proof
   that seem unfit for general public inspection.  The following
   ``fully automatic'' proof is actually a fake:
-*}
+\<close>
 
 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 
-text {*
+text \<open>
   \noindent The real source of the proof has been as follows:
 
 \begin{verbatim}
@@ -722,7 +722,7 @@
   should not misrepresent the underlying theory development.  It is
   easy to invalidate the visible text by hiding references to
   questionable axioms, for example.
-*}
+\<close>
 
 (*<*)
 end