src/Doc/Isar_Ref/Inner_Syntax.thy

   Mode names can be arbitrary, but the following ones have a specific
   meaning by convention:
 
   \begin{itemize}
 
-  \item @{verbatim "\"\""} (the empty string): default mode;
+  \item @{verbatim \<open>""\<close>} (the empty string): default mode;
   implicitly active as last element in the list of modes.
 
   \item @{verbatim input}: dummy print mode that is never active; may
   be used to specify notation that is only available for input.
 

   abbreviate general mixfix annotations as follows:
 
   \begin{center}
   \begin{tabular}{lll}
 
-  @{verbatim "("}@{keyword_def "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim "("}@{keyword_def "infix"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>} @{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
-  @{verbatim "("}@{keyword_def "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p + 1"}@{verbatim ","}~@{text "p + 1"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
+  @{verbatim "("}@{keyword_def "infixl"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>} @{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
-  @{verbatim "("}@{keyword_def "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p"}@{verbatim ","}~@{text "p + 1"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
+  @{verbatim "("}@{keyword_def "infixr"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>}~@{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p + 1"}@{verbatim ","}~@{text "p"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
 
   \end{tabular}
   \end{center}
 
-  The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ _)\""}
+  The mixfix template @{verbatim \<open>"(_\<close>}~@{text sy}@{verbatim \<open>/ _)"\<close>}
   specifies two argument positions; the delimiter is preceded by a
   space and followed by a space or line break; the entire phrase is a
   pretty printing block.
 
   The alternative notation @{verbatim "op"}~@{text sy} is introduced

   to @{cite church40}.  Isabelle declarations of certain higher-order
   operators may be annotated with @{keyword_def "binder"} annotations
   as follows:
 
   \begin{center}
-  @{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+  @{text "c :: "}@{verbatim \<open>"\<close>}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim \<open>"  (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}@{text "sy"}@{verbatim \<open>" [\<close>}@{text "p"}@{verbatim "]"}~@{text "q"}@{verbatim ")"}
   \end{center}
 
   This introduces concrete binder syntax @{text "sy x. b"}, where
   @{text x} is a bound variable of type @{text "\<tau>\<^sub>1"}, the body @{text
   b} has type @{text "\<tau>\<^sub>2"} and the whole term has type @{text "\<tau>\<^sub>3"}.

   the body; the default is @{text "q"}, which is also the priority of
   the whole construct.
 
   Internally, the binder syntax is expanded to something like this:
   \begin{center}
-  @{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+  @{text "c_binder :: "}@{verbatim \<open>"\<close>}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim \<open>"  ("(3\<close>}@{text sy}@{verbatim \<open>_./ _)" [0,\<close>}~@{text "p"}@{verbatim "]"}~@{text "q"}@{verbatim ")"}
   \end{center}
 
   Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   identifiers with optional type constraints (see also
   \secref{sec:pure-grammar}).  The mixfix template @{verbatim
-  "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions
+  \<open>"(3\<close>}@{text sy}@{verbatim \<open>_./ _)"\<close>} defines argument positions
   for the bound identifiers and the body, separated by a dot with
   optional line break; the entire phrase is a pretty printing block of
   indentation level 3.  Note that there is no extra space after @{text
   "sy"}, so it needs to be included user specification if the binder
   syntax ends with a token that may be continued by an identifier

     @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
-    @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
+    @{syntax_def (inner) string_token} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
 
   The token categories @{syntax (inner) num_token}, @{syntax (inner)

   least two) subtrees.  Occasional diagnostic output of ASTs uses
   notation that resembles S-expression of LISP.  Constant atoms are
   shown as quoted strings, variable atoms as non-quoted strings and
   applications as a parenthesized list of subtrees.  For example, the
   AST
-  @{ML [display] "Ast.Appl
-  [Ast.Constant \"_abs\", Ast.Variable \"x\", Ast.Variable \"t\"]"}
-  is pretty-printed as @{verbatim "(\"_abs\" x t)"}.  Note that
+  @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
+  is pretty-printed as @{verbatim \<open>("_abs" x t)\<close>}.  Note that
   @{verbatim "()"} and @{verbatim "(x)"} are excluded as ASTs, because
   they have too few subtrees.
 
   \medskip AST application is merely a pro-forma mechanism to indicate
   certain syntactic structures.  Thus @{verbatim "(c a b)"} could mean
   either term application or type application, depending on the
   syntactic context.
 
-  Nested application like @{verbatim "((\"_abs\" x t) u)"} is also
+  Nested application like @{verbatim \<open>(("_abs" x t) u)\<close>} is also
   possible, but ASTs are definitely first-order: the syntax constant
-  @{verbatim "\"_abs\""} does not bind the @{verbatim x} in any way.
+  @{verbatim \<open>"_abs"\<close>} does not bind the @{verbatim x} in any way.
   Proper bindings are introduced in later stages of the term syntax,
-  where @{verbatim "(\"_abs\" x t)"} becomes an @{ML Abs} node and
+  where @{verbatim \<open>("_abs" x t)\<close>} becomes an @{ML Abs} node and
   occurrences of @{verbatim x} in @{verbatim t} are replaced by bound
   variables (represented as de-Bruijn indices).
 \<close>
 
 

   constructor @{text c} (without arguments) to act as purely syntactic
   type: a nonterminal symbol of the inner syntax.
 
   \item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the
   priority grammar and the pretty printer table for the given print
-  mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref
+  mode (default @{verbatim \<open>""\<close>}). An optional keyword @{keyword_ref
   "output"} means that only the pretty printer table is affected.
 
   Following \secref{sec:mixfix}, the mixfix annotation @{text "mx =
   template ps q"} together with type @{text "\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} and
   specify a grammar production.  The @{text template} contains

   identifiers prefixed by a single underscore (e.g.\ @{text
   "_foobar"}).  Names should be chosen with care, to avoid clashes
   with other syntax declarations.
 
   \medskip The special case of copy production is specified by @{text
-  "c = "}@{verbatim "\"\""} (empty string).  It means that the
+  "c = "}@{verbatim \<open>""\<close>} (empty string).  It means that the
   resulting parse tree @{text "t"} is copied directly, without any
   further decoration.
 
   \item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
   declarations (and translations) resulting from @{text decls}, which

   input source & AST \\
   \hline
   @{text "f x y z"} & @{verbatim "(f x y z)"} \\
   @{text "'a ty"} & @{verbatim "(ty 'a)"} \\
   @{text "('a, 'b)ty"} & @{verbatim "(ty 'a 'b)"} \\
-  @{text "\<lambda>x y z. t"} & @{verbatim "(\"_abs\" x (\"_abs\" y (\"_abs\" z t)))"} \\
-  @{text "\<lambda>x :: 'a. t"} & @{verbatim "(\"_abs\" (\"_constrain\" x 'a) t)"} \\
-  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim "(\"==>\" P (\"==>\" Q (\"==>\" R S)))"} \\
-   @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim "(\"fun\" 'a (\"fun\" 'b (\"fun\" 'c 'd)))"} \\
+  @{text "\<lambda>x y z. t"} & @{verbatim \<open>("_abs" x ("_abs" y ("_abs" z t)))\<close>} \\
+  @{text "\<lambda>x :: 'a. t"} & @{verbatim \<open>("_abs" ("_constrain" x 'a) t)\<close>} \\
+  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim \<open>("==>" P ("==>" Q ("==>" R S)))\<close>} \\
+   @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim \<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close>} \\
   \end{tabular}
   \end{center}
 
   Note that type and sort constraints may occur in further places ---
   translations need to be ready to cope with them.  The built-in

   variables or constants (according to the name space), and AST
   applications to iterated term applications.
 
   The outcome is still a first-order term.  Proper abstractions and
   bound variables are introduced by parse translations associated with
-  certain syntax constants.  Thus @{verbatim "(_abs x x)"} eventually
-  becomes a de-Bruijn term @{verbatim "Abs (\"x\", _, Bound 0)"}.
+  certain syntax constants.  Thus @{verbatim \<open>("_abs" x x)\<close>} eventually
+  becomes a de-Bruijn term @{verbatim \<open>Abs ("x", _, Bound 0)\<close>}.
 \<close>
 
 
 subsubsection \<open>Printing of terms\<close>