merged
authorwenzelm
Sat Jan 09 13:31:31 2016 +0100 (2016-01-09)
changeset 62111e2b768b0035d
parent 62102 877463945ce9
parent 62110 8d75ff14e3e9
child 62112 092046740f17
merged
NEWS
     1.1 --- a/NEWS	Fri Jan 08 17:41:04 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 13:31:31 2016 +0100
     1.3 @@ -14,8 +14,18 @@
     1.4  remains available under print mode "ASCII", but less important syntax
     1.5  has been removed (see below).
     1.6  
     1.7 -* Support for more arrow symbols, with rendering in LaTeX and
     1.8 -Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>
     1.9 +* Support for more arrow symbols, with rendering in LaTeX and Isabelle
    1.10 +fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.
    1.11 +
    1.12 +* Special notation \<struct> for the first implicit 'structure' in the
    1.13 +context has been discontinued. Rare INCOMPATIBILITY, use explicit
    1.14 +structure name instead, notably in indexed notation with block-subscript
    1.15 +(e.g. \<odot>\<^bsub>A\<^esub>).
    1.16 +
    1.17 +* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
    1.18 +counterpart \<box> as quantifier-like symbol. A small diamond is available as
    1.19 +\<diamondop>; the old symbol \<struct> loses this rendering and any special
    1.20 +meaning.
    1.21  
    1.22  * Syntax for formal comments "-- text" now also supports the symbolic
    1.23  form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
     2.1 --- a/etc/symbols	Fri Jan 08 17:41:04 2016 +0100
     2.2 +++ b/etc/symbols	Sat Jan 09 13:31:31 2016 +0100
     2.3 @@ -222,6 +222,7 @@
     2.4  \<not>                  code: 0x0000ac  group: logic  abbrev: ~
     2.5  \<box>                  code: 0x0025a1  group: logic
     2.6  \<diamond>              code: 0x0025c7  group: logic
     2.7 +\<diamondop>            code: 0x0022c4  group: operator
     2.8  \<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
     2.9  \<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
    2.10  \<tturnstile>           code: 0x0022a9  group: relation  abbrev: |-
    2.11 @@ -346,7 +347,6 @@
    2.12  \<lozenge>              code: 0x0025ca
    2.13  \<wp>                   code: 0x002118
    2.14  \<wrong>                code: 0x002240  group: relation
    2.15 -\<struct>               code: 0x0022c4
    2.16  \<acute>                code: 0x0000b4
    2.17  \<index>                code: 0x000131
    2.18  \<dieresis>             code: 0x0000a8
     3.1 --- a/lib/texinputs/isabellesym.sty	Fri Jan 08 17:41:04 2016 +0100
     3.2 +++ b/lib/texinputs/isabellesym.sty	Sat Jan 09 13:31:31 2016 +0100
     3.3 @@ -220,16 +220,17 @@
     3.4  \newcommand{\isasymOr}{\isamath{\bigvee}}
     3.5  \newcommand{\isasymforall}{\isamath{\forall\,}}
     3.6  \newcommand{\isasymexists}{\isamath{\exists\,}}
     3.7 +\newcommand{\isasymnot}{\isamath{\neg}}
     3.8  \newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
     3.9 -\newcommand{\isasymnot}{\isamath{\neg}}
    3.10  \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
    3.11  \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
    3.12 +\newcommand{\isasymdiamondop}{\isamath{\diamond}}
    3.13 +\newcommand{\isasymsurd}{\isamath{\surd}}
    3.14  \newcommand{\isasymturnstile}{\isamath{\vdash}}
    3.15  \newcommand{\isasymTurnstile}{\isamath{\models}}
    3.16  \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
    3.17  \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
    3.18  \newcommand{\isasymstileturn}{\isamath{\dashv}}
    3.19 -\newcommand{\isasymsurd}{\isamath{\surd}}
    3.20  \newcommand{\isasymle}{\isamath{\le}}
    3.21  \newcommand{\isasymge}{\isamath{\ge}}
    3.22  \newcommand{\isasymlless}{\isamath{\ll}}
    3.23 @@ -350,7 +351,6 @@
    3.24  \newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
    3.25  \newcommand{\isasymwp}{\isamath{\wp}}
    3.26  \newcommand{\isasymwrong}{\isamath{\wr}}
    3.27 -\newcommand{\isasymstruct}{\isamath{\diamond}}
    3.28  \newcommand{\isasymacute}{\isatext{\'\relax}}
    3.29  \newcommand{\isasymindex}{\isatext{\i}}
    3.30  \newcommand{\isasymdieresis}{\isatext{\"\relax}}
     4.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 17:41:04 2016 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 09 13:31:31 2016 +0100
     4.3 @@ -6,26 +6,25 @@
     4.4  
     4.5  chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
     4.6  
     4.7 -text \<open>The inner syntax of Isabelle provides concrete notation for
     4.8 -  the main entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type classes.  Applications may either
     4.9 -  extend existing syntactic categories by additional notation, or
    4.10 -  define new sub-languages that are linked to the standard term
    4.11 -  language via some explicit markers.  For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close> could
    4.12 -  embed the syntax corresponding for some
    4.13 -  user-defined nonterminal \<open>foo\<close> --- within the bounds of the
    4.14 -  given lexical syntax of Isabelle/Pure.
    4.15 +text \<open>
    4.16 +  The inner syntax of Isabelle provides concrete notation for the main
    4.17 +  entities of the logical framework, notably \<open>\<lambda>\<close>-terms with types and type
    4.18 +  classes. Applications may either extend existing syntactic categories by
    4.19 +  additional notation, or define new sub-languages that are linked to the
    4.20 +  standard term language via some explicit markers. For example \<^verbatim>\<open>FOO\<close>~\<open>foo\<close>
    4.21 +  could embed the syntax corresponding for some user-defined nonterminal \<open>foo\<close>
    4.22 +  --- within the bounds of the given lexical syntax of Isabelle/Pure.
    4.23  
    4.24 -  The most basic way to specify concrete syntax for logical entities
    4.25 -  works via mixfix annotations (\secref{sec:mixfix}), which may be
    4.26 -  usually given as part of the original declaration or via explicit
    4.27 -  notation commands later on (\secref{sec:notation}).  This already
    4.28 -  covers many needs of concrete syntax without having to understand
    4.29 -  the full complexity of inner syntax layers.
    4.30 +  The most basic way to specify concrete syntax for logical entities works via
    4.31 +  mixfix annotations (\secref{sec:mixfix}), which may be usually given as part
    4.32 +  of the original declaration or via explicit notation commands later on
    4.33 +  (\secref{sec:notation}). This already covers many needs of concrete syntax
    4.34 +  without having to understand the full complexity of inner syntax layers.
    4.35  
    4.36 -  Further details of the syntax engine involves the classical
    4.37 -  distinction of lexical language versus context-free grammar (see
    4.38 -  \secref{sec:pure-syntax}), and various mechanisms for \<^emph>\<open>syntax
    4.39 -  transformations\<close> (see \secref{sec:syntax-transformations}).
    4.40 +  Further details of the syntax engine involves the classical distinction of
    4.41 +  lexical language versus context-free grammar (see \secref{sec:pure-syntax}),
    4.42 +  and various mechanisms for \<^emph>\<open>syntax transformations\<close> (see
    4.43 +  \secref{sec:syntax-transformations}).
    4.44  \<close>
    4.45  
    4.46  
    4.47 @@ -63,43 +62,39 @@
    4.48      @{syntax_def modes}: '(' (@{syntax name} + ) ')'
    4.49    \<close>}
    4.50  
    4.51 -  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression
    4.52 -  according to the current context.
    4.53 +  \<^descr> @{command "typ"}~\<open>\<tau>\<close> reads and prints a type expression according to the
    4.54 +  current context.
    4.55  
    4.56 -  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to
    4.57 -  determine the most general way to make \<open>\<tau>\<close> conform to sort
    4.58 -  \<open>s\<close>.  For concrete \<open>\<tau>\<close> this checks if the type
    4.59 -  belongs to that sort.  Dummy type parameters ``\<open>_\<close>''
    4.60 -  (underscore) are assigned to fresh type variables with most general
    4.61 -  sorts, according the the principles of type-inference.
    4.62 +  \<^descr> @{command "typ"}~\<open>\<tau> :: s\<close> uses type-inference to determine the most
    4.63 +  general way to make \<open>\<tau>\<close> conform to sort \<open>s\<close>. For concrete \<open>\<tau>\<close> this checks if
    4.64 +  the type belongs to that sort. Dummy type parameters ``\<open>_\<close>'' (underscore)
    4.65 +  are assigned to fresh type variables with most general sorts, according the
    4.66 +  the principles of type-inference.
    4.67  
    4.68 -  \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close>
    4.69 -  read, type-check and print terms or propositions according to the
    4.70 -  current theory or proof context; the inferred type of \<open>t\<close> is
    4.71 -  output as well.  Note that these commands are also useful in
    4.72 -  inspecting the current environment of term abbreviations.
    4.73 +    \<^descr> @{command "term"}~\<open>t\<close> and @{command "prop"}~\<open>\<phi>\<close> read, type-check and
    4.74 +    print terms or propositions according to the current theory or proof
    4.75 +    context; the inferred type of \<open>t\<close> is output as well. Note that these
    4.76 +    commands are also useful in inspecting the current environment of term
    4.77 +    abbreviations.
    4.78  
    4.79 -  \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves
    4.80 -  theorems from the current theory or proof context.  Note that any
    4.81 -  attributes included in the theorem specifications are applied to a
    4.82 -  temporary context derived from the current theory or proof; the
    4.83 -  result is discarded, i.e.\ attributes involved in \<open>a\<^sub>1,
    4.84 -  \<dots>, a\<^sub>n\<close> do not have any permanent effect.
    4.85 +    \<^descr> @{command "thm"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> retrieves theorems from the current theory
    4.86 +    or proof context. Note that any attributes included in the theorem
    4.87 +    specifications are applied to a temporary context derived from the current
    4.88 +    theory or proof; the result is discarded, i.e.\ attributes involved in
    4.89 +    \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
    4.90  
    4.91 -  \<^descr> @{command "prf"} displays the (compact) proof term of the
    4.92 -  current proof state (if present), or of the given theorems. Note
    4.93 -  that this requires proof terms to be switched on for the current
    4.94 -  object logic (see the ``Proof terms'' section of the Isabelle
    4.95 -  reference manual for information on how to do this).
    4.96 +    \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
    4.97 +    state (if present), or of the given theorems. Note that this requires
    4.98 +    proof terms to be switched on for the current object logic (see the
    4.99 +    ``Proof terms'' section of the Isabelle reference manual for information
   4.100 +    on how to do this).
   4.101  
   4.102 -  \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays
   4.103 -  the full proof term, i.e.\ also displays information omitted in the
   4.104 -  compact proof term, which is denoted by ``\<open>_\<close>'' placeholders
   4.105 -  there.
   4.106 +    \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
   4.107 +    proof term, i.e.\ also displays information omitted in the compact proof
   4.108 +    term, which is denoted by ``\<open>_\<close>'' placeholders there.
   4.109  
   4.110 -  \<^descr> @{command "print_state"} prints the current proof state (if
   4.111 -  present), including current facts and goals.
   4.112 -
   4.113 +    \<^descr> @{command "print_state"} prints the current proof state (if present),
   4.114 +    including current facts and goals.
   4.115  
   4.116    All of the diagnostic commands above admit a list of \<open>modes\<close> to be
   4.117    specified, which is appended to the current print mode; see also
   4.118 @@ -109,9 +104,8 @@
   4.119    symbols and special characters represented in {\LaTeX} source, according to
   4.120    the Isabelle style @{cite "isabelle-system"}.
   4.121  
   4.122 -  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   4.123 -  systematic way to include formal items into the printed text
   4.124 -  document.
   4.125 +  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
   4.126 +  way to include formal items into the printed text document.
   4.127  \<close>
   4.128  
   4.129  
   4.130 @@ -137,100 +131,90 @@
   4.131    \end{tabular}
   4.132    \<^medskip>
   4.133  
   4.134 -  These configuration options control the detail of information that
   4.135 -  is displayed for types, terms, theorems, goals etc.  See also
   4.136 +  These configuration options control the detail of information that is
   4.137 +  displayed for types, terms, theorems, goals etc. See also
   4.138    \secref{sec:config}.
   4.139  
   4.140 -  \<^descr> @{attribute show_markup} controls direct inlining of markup
   4.141 -  into the printed representation of formal entities --- notably type
   4.142 -  and sort constraints.  This enables Prover IDE users to retrieve
   4.143 -  that information via tooltips or popups while hovering with the
   4.144 -  mouse over the output window, for example.  Consequently, this
   4.145 -  option is enabled by default for Isabelle/jEdit.
   4.146 +  \<^descr> @{attribute show_markup} controls direct inlining of markup into the
   4.147 +  printed representation of formal entities --- notably type and sort
   4.148 +  constraints. This enables Prover IDE users to retrieve that information via
   4.149 +  tooltips or popups while hovering with the mouse over the output window, for
   4.150 +  example. Consequently, this option is enabled by default for Isabelle/jEdit.
   4.151  
   4.152 -  \<^descr> @{attribute show_types} and @{attribute show_sorts} control
   4.153 -  printing of type constraints for term variables, and sort
   4.154 -  constraints for type variables.  By default, neither of these are
   4.155 -  shown in output.  If @{attribute show_sorts} is enabled, types are
   4.156 -  always shown as well.  In Isabelle/jEdit, manual setting of these
   4.157 -  options is normally not required thanks to @{attribute show_markup}
   4.158 -  above.
   4.159 +  \<^descr> @{attribute show_types} and @{attribute show_sorts} control printing of
   4.160 +  type constraints for term variables, and sort constraints for type
   4.161 +  variables. By default, neither of these are shown in output. If @{attribute
   4.162 +  show_sorts} is enabled, types are always shown as well. In Isabelle/jEdit,
   4.163 +  manual setting of these options is normally not required thanks to
   4.164 +  @{attribute show_markup} above.
   4.165  
   4.166 -  Note that displaying types and sorts may explain why a polymorphic
   4.167 -  inference rule fails to resolve with some goal, or why a rewrite
   4.168 -  rule does not apply as expected.
   4.169 -
   4.170 -  \<^descr> @{attribute show_consts} controls printing of types of
   4.171 -  constants when displaying a goal state.
   4.172 +  Note that displaying types and sorts may explain why a polymorphic inference
   4.173 +  rule fails to resolve with some goal, or why a rewrite rule does not apply
   4.174 +  as expected.
   4.175  
   4.176 -  Note that the output can be enormous, because polymorphic constants
   4.177 -  often occur at several different type instances.
   4.178 +  \<^descr> @{attribute show_consts} controls printing of types of constants when
   4.179 +  displaying a goal state.
   4.180  
   4.181 -  \<^descr> @{attribute show_abbrevs} controls folding of constant
   4.182 -  abbreviations.
   4.183 +  Note that the output can be enormous, because polymorphic constants often
   4.184 +  occur at several different type instances.
   4.185 +
   4.186 +  \<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
   4.187  
   4.188 -  \<^descr> @{attribute show_brackets} controls bracketing in pretty
   4.189 -  printed output.  If enabled, all sub-expressions of the pretty
   4.190 -  printing tree will be parenthesized, even if this produces malformed
   4.191 -  term syntax!  This crude way of showing the internal structure of
   4.192 -  pretty printed entities may occasionally help to diagnose problems
   4.193 -  with operator priorities, for example.
   4.194 +  \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
   4.195 +  If enabled, all sub-expressions of the pretty printing tree will be
   4.196 +  parenthesized, even if this produces malformed term syntax! This crude way
   4.197 +  of showing the internal structure of pretty printed entities may
   4.198 +  occasionally help to diagnose problems with operator priorities, for
   4.199 +  example.
   4.200  
   4.201 -  \<^descr> @{attribute names_long}, @{attribute names_short}, and
   4.202 -  @{attribute names_unique} control the way of printing fully
   4.203 -  qualified internal names in external form.  See also
   4.204 -  \secref{sec:antiq} for the document antiquotation options of the
   4.205 -  same names.
   4.206 +  \<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
   4.207 +  names_unique} control the way of printing fully qualified internal names in
   4.208 +  external form. See also \secref{sec:antiq} for the document antiquotation
   4.209 +  options of the same names.
   4.210  
   4.211 -  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted
   4.212 -  printing of terms.
   4.213 +  \<^descr> @{attribute eta_contract} controls \<open>\<eta>\<close>-contracted printing of terms.
   4.214  
   4.215 -  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"},
   4.216 -  provided \<open>x\<close> is not free in \<open>f\<close>.  It asserts
   4.217 -  \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if @{prop "f x \<equiv>
   4.218 -  g x"} for all \<open>x\<close>.  Higher-order unification frequently puts
   4.219 -  terms into a fully \<open>\<eta>\<close>-expanded form.  For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>) \<Rightarrow> \<tau>\<close> then its expanded form is @{term
   4.220 -  "\<lambda>h. F (\<lambda>x. h x)"}.
   4.221 +  The \<open>\<eta>\<close>-contraction law asserts @{prop "(\<lambda>x. f x) \<equiv> f"}, provided \<open>x\<close> is not
   4.222 +  free in \<open>f\<close>. It asserts \<^emph>\<open>extensionality\<close> of functions: @{prop "f \<equiv> g"} if
   4.223 +  @{prop "f x \<equiv> g x"} for all \<open>x\<close>. Higher-order unification frequently puts
   4.224 +  terms into a fully \<open>\<eta>\<close>-expanded form. For example, if \<open>F\<close> has type \<open>(\<tau> \<Rightarrow> \<tau>)
   4.225 +  \<Rightarrow> \<tau>\<close> then its expanded form is @{term "\<lambda>h. F (\<lambda>x. h x)"}.
   4.226  
   4.227 -  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"}
   4.228 -  appears simply as \<open>F\<close>.
   4.229 +  Enabling @{attribute eta_contract} makes Isabelle perform \<open>\<eta>\<close>-contractions
   4.230 +  before printing, so that @{term "\<lambda>h. F (\<lambda>x. h x)"} appears simply as \<open>F\<close>.
   4.231  
   4.232 -  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded
   4.233 -  form occasionally matters.  While higher-order resolution and
   4.234 -  rewriting operate modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools
   4.235 -  might look at terms more discretely.
   4.236 +  Note that the distinction between a term and its \<open>\<eta>\<close>-expanded form
   4.237 +  occasionally matters. While higher-order resolution and rewriting operate
   4.238 +  modulo \<open>\<alpha>\<beta>\<eta>\<close>-conversion, some other tools might look at terms more
   4.239 +  discretely.
   4.240  
   4.241 -  \<^descr> @{attribute goals_limit} controls the maximum number of
   4.242 -  subgoals to be printed.
   4.243 +  \<^descr> @{attribute goals_limit} controls the maximum number of subgoals to be
   4.244 +  printed.
   4.245  
   4.246 -  \<^descr> @{attribute show_main_goal} controls whether the main result
   4.247 -  to be proven should be displayed.  This information might be
   4.248 -  relevant for schematic goals, to inspect the current claim that has
   4.249 -  been synthesized so far.
   4.250 +  \<^descr> @{attribute show_main_goal} controls whether the main result to be proven
   4.251 +  should be displayed. This information might be relevant for schematic goals,
   4.252 +  to inspect the current claim that has been synthesized so far.
   4.253  
   4.254 -  \<^descr> @{attribute show_hyps} controls printing of implicit
   4.255 -  hypotheses of local facts.  Normally, only those hypotheses are
   4.256 -  displayed that are \<^emph>\<open>not\<close> covered by the assumptions of the
   4.257 -  current context: this situation indicates a fault in some tool being
   4.258 -  used.
   4.259 +  \<^descr> @{attribute show_hyps} controls printing of implicit hypotheses of local
   4.260 +  facts. Normally, only those hypotheses are displayed that are \<^emph>\<open>not\<close> covered
   4.261 +  by the assumptions of the current context: this situation indicates a fault
   4.262 +  in some tool being used.
   4.263  
   4.264 -  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses
   4.265 -  can be enforced, which is occasionally useful for diagnostic
   4.266 -  purposes.
   4.267 +  By enabling @{attribute show_hyps}, output of \<^emph>\<open>all\<close> hypotheses can be
   4.268 +  enforced, which is occasionally useful for diagnostic purposes.
   4.269  
   4.270 -  \<^descr> @{attribute show_tags} controls printing of extra annotations
   4.271 -  within theorems, such as internal position information, or the case
   4.272 -  names being attached by the attribute @{attribute case_names}.
   4.273 +  \<^descr> @{attribute show_tags} controls printing of extra annotations within
   4.274 +  theorems, such as internal position information, or the case names being
   4.275 +  attached by the attribute @{attribute case_names}.
   4.276  
   4.277 -  Note that the @{attribute tagged} and @{attribute untagged}
   4.278 -  attributes provide low-level access to the collection of tags
   4.279 -  associated with a theorem.
   4.280 +  Note that the @{attribute tagged} and @{attribute untagged} attributes
   4.281 +  provide low-level access to the collection of tags associated with a
   4.282 +  theorem.
   4.283  
   4.284 -  \<^descr> @{attribute show_question_marks} controls printing of question
   4.285 -  marks for schematic variables, such as \<open>?x\<close>.  Only the leading
   4.286 -  question mark is affected, the remaining text is unchanged
   4.287 -  (including proper markup for schematic variables that might be
   4.288 -  relevant for user interfaces).
   4.289 +  \<^descr> @{attribute show_question_marks} controls printing of question marks for
   4.290 +  schematic variables, such as \<open>?x\<close>. Only the leading question mark is
   4.291 +  affected, the remaining text is unchanged (including proper markup for
   4.292 +  schematic variables that might be relevant for user interfaces).
   4.293  \<close>
   4.294  
   4.295  
   4.296 @@ -242,62 +226,58 @@
   4.297      @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
   4.298    \end{mldecls}
   4.299  
   4.300 -  The \<^emph>\<open>print mode\<close> facility allows to modify various operations
   4.301 -  for printing.  Commands like @{command typ}, @{command term},
   4.302 -  @{command thm} (see \secref{sec:print-diag}) take additional print
   4.303 -  modes as optional argument.  The underlying ML operations are as
   4.304 -  follows.
   4.305 +  The \<^emph>\<open>print mode\<close> facility allows to modify various operations for printing.
   4.306 +  Commands like @{command typ}, @{command term}, @{command thm} (see
   4.307 +  \secref{sec:print-diag}) take additional print modes as optional argument.
   4.308 +  The underlying ML operations are as follows.
   4.309  
   4.310 -  \<^descr> @{ML "print_mode_value ()"} yields the list of currently
   4.311 -  active print mode names.  This should be understood as symbolic
   4.312 -  representation of certain individual features for printing (with
   4.313 -  precedence from left to right).
   4.314 +    \<^descr> @{ML "print_mode_value ()"} yields the list of currently active print
   4.315 +    mode names. This should be understood as symbolic representation of
   4.316 +    certain individual features for printing (with precedence from left to
   4.317 +    right).
   4.318  
   4.319 -  \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates
   4.320 -  \<open>f x\<close> in an execution context where the print mode is
   4.321 -  prepended by the given \<open>modes\<close>.  This provides a thread-safe
   4.322 -  way to augment print modes.  It is also monotonic in the set of mode
   4.323 -  names: it retains the default print mode that certain
   4.324 -  user-interfaces might have installed for their proper functioning!
   4.325 -
   4.326 +    \<^descr> @{ML Print_Mode.with_modes}~\<open>modes f x\<close> evaluates \<open>f x\<close> in an execution
   4.327 +    context where the print mode is prepended by the given \<open>modes\<close>. This
   4.328 +    provides a thread-safe way to augment print modes. It is also monotonic in
   4.329 +    the set of mode names: it retains the default print mode that certain
   4.330 +    user-interfaces might have installed for their proper functioning!
   4.331  
   4.332    \<^medskip>
   4.333 -  The pretty printer for inner syntax maintains alternative
   4.334 -  mixfix productions for any print mode name invented by the user, say
   4.335 -  in commands like @{command notation} or @{command abbreviation}.
   4.336 -  Mode names can be arbitrary, but the following ones have a specific
   4.337 -  meaning by convention:
   4.338 +  The pretty printer for inner syntax maintains alternative mixfix productions
   4.339 +  for any print mode name invented by the user, say in commands like @{command
   4.340 +  notation} or @{command abbreviation}. Mode names can be arbitrary, but the
   4.341 +  following ones have a specific meaning by convention:
   4.342  
   4.343 -  \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode;
   4.344 -  implicitly active as last element in the list of modes.
   4.345 +    \<^item> \<^verbatim>\<open>""\<close> (the empty string): default mode; implicitly active as last
   4.346 +    element in the list of modes.
   4.347  
   4.348 -  \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may
   4.349 -  be used to specify notation that is only available for input.
   4.350 +    \<^item> \<^verbatim>\<open>input\<close>: dummy print mode that is never active; may be used to specify
   4.351 +    notation that is only available for input.
   4.352  
   4.353 -  \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
   4.354 -  used internally in Isabelle/Pure.
   4.355 +    \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active; used internally in
   4.356 +    Isabelle/Pure.
   4.357  
   4.358 -  \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
   4.359 +    \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
   4.360  
   4.361 -  \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
   4.362 -  document preparation of Isabelle theory sources; allows to provide
   4.363 -  alternative output notation.
   4.364 +    \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX} document
   4.365 +    preparation of Isabelle theory sources; allows to provide alternative
   4.366 +    output notation.
   4.367  \<close>
   4.368  
   4.369  
   4.370  section \<open>Mixfix annotations \label{sec:mixfix}\<close>
   4.371  
   4.372 -text \<open>Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of
   4.373 -  Isabelle types and terms.  Locally fixed parameters in toplevel
   4.374 -  theorem statements, locale and class specifications also admit
   4.375 -  mixfix annotations in a fairly uniform manner.  A mixfix annotation
   4.376 -  describes the concrete syntax, the translation to abstract
   4.377 -  syntax, and the pretty printing.  Special case annotations provide a
   4.378 -  simple means of specifying infix operators and binders.
   4.379 +text \<open>
   4.380 +  Mixfix annotations specify concrete \<^emph>\<open>inner syntax\<close> of Isabelle types and
   4.381 +  terms. Locally fixed parameters in toplevel theorem statements, locale and
   4.382 +  class specifications also admit mixfix annotations in a fairly uniform
   4.383 +  manner. A mixfix annotation describes the concrete syntax, the translation
   4.384 +  to abstract syntax, and the pretty printing. Special case annotations
   4.385 +  provide a simple means of specifying infix operators and binders.
   4.386  
   4.387 -  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}.  It allows
   4.388 -  to specify any context-free priority grammar, which is more general
   4.389 -  than the fixity declarations of ML and Prolog.
   4.390 +  Isabelle mixfix syntax is inspired by {\OBJ} @{cite OBJ}. It allows to
   4.391 +  specify any context-free priority grammar, which is more general than the
   4.392 +  fixity declarations of ML and Prolog.
   4.393  
   4.394    @{rail \<open>
   4.395      @{syntax_def mixfix}: '('
   4.396 @@ -311,52 +291,48 @@
   4.397      prios: '[' (@{syntax nat} + ',') ']'
   4.398    \<close>}
   4.399  
   4.400 -  The string given as \<open>template\<close> may include literal text,
   4.401 -  spacing, blocks, and arguments (denoted by ``\<open>_\<close>''); the
   4.402 -  special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as ``\<open>\<index>\<close>'')
   4.403 -  represents an index argument that specifies an implicit @{keyword
   4.404 -  "structure"} reference (see also \secref{sec:locale}).  Only locally
   4.405 -  fixed variables may be declared as @{keyword "structure"}.
   4.406 +  The string given as \<open>template\<close> may include literal text, spacing, blocks,
   4.407 +  and arguments (denoted by ``\<open>_\<close>''); the special symbol ``\<^verbatim>\<open>\<index>\<close>'' (printed as
   4.408 +  ``\<open>\<index>\<close>'') represents an index argument that specifies an implicit @{keyword
   4.409 +  "structure"} reference (see also \secref{sec:locale}). Only locally fixed
   4.410 +  variables may be declared as @{keyword "structure"}.
   4.411  
   4.412 -  Infix and binder declarations provide common abbreviations for
   4.413 -  particular mixfix declarations.  So in practice, mixfix templates
   4.414 -  mostly degenerate to literal text for concrete syntax, such as
   4.415 -  ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
   4.416 +  Infix and binder declarations provide common abbreviations for particular
   4.417 +  mixfix declarations. So in practice, mixfix templates mostly degenerate to
   4.418 +  literal text for concrete syntax, such as ``\<^verbatim>\<open>++\<close>'' for an infix symbol.
   4.419  \<close>
   4.420  
   4.421  
   4.422  subsection \<open>The general mixfix form\<close>
   4.423  
   4.424 -text \<open>In full generality, mixfix declarations work as follows.
   4.425 -  Suppose a constant \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by
   4.426 -  \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where \<open>mixfix\<close> is a string
   4.427 -  \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that surround
   4.428 -  argument positions as indicated by underscores.
   4.429 +text \<open>
   4.430 +  In full generality, mixfix declarations work as follows. Suppose a constant
   4.431 +  \<open>c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> is annotated by \<open>(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)\<close>, where
   4.432 +  \<open>mixfix\<close> is a string \<open>d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n\<close> consisting of delimiters that
   4.433 +  surround argument positions as indicated by underscores.
   4.434  
   4.435 -  Altogether this determines a production for a context-free priority
   4.436 -  grammar, where for each argument \<open>i\<close> the syntactic category
   4.437 -  is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the
   4.438 -  result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>).  Priority specifications are optional, with default 0 for
   4.439 -  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is
   4.440 -  prone to syntactic ambiguities unless the delimiter tokens determine
   4.441 -  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
   4.442 +  Altogether this determines a production for a context-free priority grammar,
   4.443 +  where for each argument \<open>i\<close> the syntactic category is determined by \<open>\<tau>\<^sub>i\<close>
   4.444 +  (with priority \<open>p\<^sub>i\<close>), and the result category is determined from \<open>\<tau>\<close> (with
   4.445 +  priority \<open>p\<close>). Priority specifications are optional, with default 0 for
   4.446 +  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is prone to
   4.447 +  syntactic ambiguities unless the delimiter tokens determine fully bracketed
   4.448 +  notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
   4.449  
   4.450 -  Since \<open>\<tau>\<close> may be again a function type, the constant
   4.451 -  type scheme may have more argument positions than the mixfix
   4.452 -  pattern.  Printing a nested application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for
   4.453 -  \<open>m > n\<close> works by attaching concrete notation only to the
   4.454 -  innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
   4.455 -  instead.  If a term has fewer arguments than specified in the mixfix
   4.456 +  Since \<open>\<tau>\<close> may be again a function type, the constant type scheme may have
   4.457 +  more argument positions than the mixfix pattern. Printing a nested
   4.458 +  application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for \<open>m > n\<close> works by attaching concrete notation
   4.459 +  only to the innermost part, essentially by printing \<open>(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m\<close>
   4.460 +  instead. If a term has fewer arguments than specified in the mixfix
   4.461    template, the concrete syntax is ignored.
   4.462  
   4.463    \<^medskip>
   4.464 -  A mixfix template may also contain additional directives
   4.465 -  for pretty printing, notably spaces, blocks, and breaks.  The
   4.466 -  general template format is a sequence over any of the following
   4.467 -  entities.
   4.468 +  A mixfix template may also contain additional directives for pretty
   4.469 +  printing, notably spaces, blocks, and breaks. The general template format is
   4.470 +  a sequence over any of the following entities.
   4.471  
   4.472 -  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of
   4.473 -  characters other than the following special characters:
   4.474 +  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
   4.475 +  the following special characters:
   4.476  
   4.477    \<^medskip>
   4.478    \begin{tabular}{ll}
   4.479 @@ -369,47 +345,45 @@
   4.480    \end{tabular}
   4.481    \<^medskip>
   4.482  
   4.483 -  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these
   4.484 -  meta-characters, producing a literal version of the following
   4.485 -  character, unless that is a blank.
   4.486 +  \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
   4.487 +  literal version of the following character, unless that is a blank.
   4.488  
   4.489 -  A single quote followed by a blank separates delimiters, without
   4.490 -  affecting printing, but input tokens may have additional white space
   4.491 -  here.
   4.492 +  A single quote followed by a blank separates delimiters, without affecting
   4.493 +  printing, but input tokens may have additional white space here.
   4.494  
   4.495 -  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a
   4.496 -  certain syntactic category in the underlying grammar.
   4.497 +  \<^descr> \<^verbatim>\<open>_\<close> is an argument position, which stands for a certain syntactic
   4.498 +  category in the underlying grammar.
   4.499  
   4.500 -  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place
   4.501 -  where implicit structure arguments can be attached.
   4.502 -
   4.503 -  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing.
   4.504 -  This and the following specifications do not affect parsing at all.
   4.505 +  \<^descr> \<open>\<index>\<close> is an indexed argument position; this is the place where implicit
   4.506 +  structure arguments can be attached.
   4.507  
   4.508 -  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block.  The
   4.509 -  optional number specifies how much indentation to add when a line
   4.510 -  break occurs within the block.  If the parenthesis is not followed
   4.511 -  by digits, the indentation defaults to 0.  A block specified via
   4.512 -  \<^verbatim>\<open>(00\<close> is unbreakable.
   4.513 +  \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following
   4.514 +  specifications do not affect parsing at all.
   4.515 +
   4.516 +  \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how
   4.517 +  much indentation to add when a line break occurs within the block. If the
   4.518 +  parenthesis is not followed by digits, the indentation defaults to 0. A
   4.519 +  block specified via \<^verbatim>\<open>(00\<close> is unbreakable.
   4.520  
   4.521    \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
   4.522  
   4.523    \<^descr> \<^verbatim>\<open>//\<close> forces a line break.
   4.524  
   4.525 -  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break.  Here \<open>s\<close>
   4.526 -  stands for the string of spaces (zero or more) right after the
   4.527 -  slash.  These spaces are printed if the break is \<^emph>\<open>not\<close> taken.
   4.528 +  \<^descr> \<^verbatim>\<open>/\<close>\<open>s\<close> allows a line break. Here \<open>s\<close> stands for the string of spaces
   4.529 +  (zero or more) right after the slash. These spaces are printed if the break
   4.530 +  is \<^emph>\<open>not\<close> taken.
   4.531  
   4.532  
   4.533 -  The general idea of pretty printing with blocks and breaks is also
   4.534 -  described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
   4.535 +  The general idea of pretty printing with blocks and breaks is also described
   4.536 +  in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
   4.537  \<close>
   4.538  
   4.539  
   4.540  subsection \<open>Infixes\<close>
   4.541  
   4.542 -text \<open>Infix operators are specified by convenient short forms that
   4.543 -  abbreviate general mixfix annotations as follows:
   4.544 +text \<open>
   4.545 +  Infix operators are specified by convenient short forms that abbreviate
   4.546 +  general mixfix annotations as follows:
   4.547  
   4.548    \begin{center}
   4.549    \begin{tabular}{lll}
   4.550 @@ -427,35 +401,33 @@
   4.551    \end{tabular}
   4.552    \end{center}
   4.553  
   4.554 -  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close>
   4.555 -  specifies two argument positions; the delimiter is preceded by a
   4.556 -  space and followed by a space or line break; the entire phrase is a
   4.557 -  pretty printing block.
   4.558 +  The mixfix template \<^verbatim>\<open>"(_\<close>~\<open>sy\<close>\<^verbatim>\<open>/ _)"\<close> specifies two argument positions;
   4.559 +  the delimiter is preceded by a space and followed by a space or line break;
   4.560 +  the entire phrase is a pretty printing block.
   4.561  
   4.562 -  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced
   4.563 -  in addition.  Thus any infix operator may be written in prefix form
   4.564 -  (as in ML), independently of the number of arguments in the term.
   4.565 +  The alternative notation \<^verbatim>\<open>op\<close>~\<open>sy\<close> is introduced in addition. Thus any
   4.566 +  infix operator may be written in prefix form (as in ML), independently of
   4.567 +  the number of arguments in the term.
   4.568  \<close>
   4.569  
   4.570  
   4.571  subsection \<open>Binders\<close>
   4.572  
   4.573 -text \<open>A \<^emph>\<open>binder\<close> is a variable-binding construct such as a
   4.574 -  quantifier.  The idea to formalize \<open>\<forall>x. b\<close> as \<open>All
   4.575 -  (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> already goes back
   4.576 -  to @{cite church40}.  Isabelle declarations of certain higher-order
   4.577 -  operators may be annotated with @{keyword_def "binder"} annotations
   4.578 -  as follows:
   4.579 +text \<open>
   4.580 +  A \<^emph>\<open>binder\<close> is a variable-binding construct such as a quantifier. The idea
   4.581 +  to formalize \<open>\<forall>x. b\<close> as \<open>All (\<lambda>x. b)\<close> for \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close>
   4.582 +  already goes back to @{cite church40}. Isabelle declarations of certain
   4.583 +  higher-order operators may be annotated with @{keyword_def "binder"}
   4.584 +  annotations as follows:
   4.585  
   4.586    \begin{center}
   4.587    \<open>c ::\<close>~\<^verbatim>\<open>"\<close>\<open>(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3\<close>\<^verbatim>\<open>"  (\<close>@{keyword "binder"}~\<^verbatim>\<open>"\<close>\<open>sy\<close>\<^verbatim>\<open>" [\<close>\<open>p\<close>\<^verbatim>\<open>]\<close>~\<open>q\<close>\<^verbatim>\<open>)\<close>
   4.588    \end{center}
   4.589  
   4.590 -  This introduces concrete binder syntax \<open>sy x. b\<close>, where
   4.591 -  \<open>x\<close> is a bound variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has type \<open>\<tau>\<^sub>3\<close>.
   4.592 -  The optional integer \<open>p\<close> specifies the syntactic priority of
   4.593 -  the body; the default is \<open>q\<close>, which is also the priority of
   4.594 -  the whole construct.
   4.595 +  This introduces concrete binder syntax \<open>sy x. b\<close>, where \<open>x\<close> is a bound
   4.596 +  variable of type \<open>\<tau>\<^sub>1\<close>, the body \<open>b\<close> has type \<open>\<tau>\<^sub>2\<close> and the whole term has
   4.597 +  type \<open>\<tau>\<^sub>3\<close>. The optional integer \<open>p\<close> specifies the syntactic priority of the
   4.598 +  body; the default is \<open>q\<close>, which is also the priority of the whole construct.
   4.599  
   4.600    Internally, the binder syntax is expanded to something like this:
   4.601    \begin{center}
   4.602 @@ -464,17 +436,18 @@
   4.603  
   4.604    Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   4.605    identifiers with optional type constraints (see also
   4.606 -  \secref{sec:pure-grammar}).  The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close>
   4.607 -  defines argument positions
   4.608 -  for the bound identifiers and the body, separated by a dot with
   4.609 -  optional line break; the entire phrase is a pretty printing block of
   4.610 -  indentation level 3.  Note that there is no extra space after \<open>sy\<close>, so it needs to be included user specification if the binder
   4.611 -  syntax ends with a token that may be continued by an identifier
   4.612 -  token at the start of @{syntax (inner) idts}.
   4.613 +  \secref{sec:pure-grammar}). The mixfix template \<^verbatim>\<open>"(3\<close>\<open>sy\<close>\<^verbatim>\<open>_./ _)"\<close> defines
   4.614 +  argument positions for the bound identifiers and the body, separated by a
   4.615 +  dot with optional line break; the entire phrase is a pretty printing block
   4.616 +  of indentation level 3. Note that there is no extra space after \<open>sy\<close>, so it
   4.617 +  needs to be included user specification if the binder syntax ends with a
   4.618 +  token that may be continued by an identifier token at the start of @{syntax
   4.619 +  (inner) idts}.
   4.620  
   4.621 -  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1
   4.622 -  \<dots> x\<^sub>n b\<close> into iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>.
   4.623 -  This works in both directions, for parsing and printing.\<close>
   4.624 +  Furthermore, a syntax translation to transforms \<open>c_binder x\<^sub>1 \<dots> x\<^sub>n b\<close> into
   4.625 +  iterated application \<open>c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)\<close>. This works in both
   4.626 +  directions, for parsing and printing.
   4.627 +\<close>
   4.628  
   4.629  
   4.630  section \<open>Explicit notation \label{sec:notation}\<close>
   4.631 @@ -488,12 +461,11 @@
   4.632      @{command_def "write"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   4.633    \end{matharray}
   4.634  
   4.635 -  Commands that introduce new logical entities (terms or types)
   4.636 -  usually allow to provide mixfix annotations on the spot, which is
   4.637 -  convenient for default notation.  Nonetheless, the syntax may be
   4.638 -  modified later on by declarations for explicit notation.  This
   4.639 -  allows to add or delete mixfix annotations for of existing logical
   4.640 -  entities within the current context.
   4.641 +  Commands that introduce new logical entities (terms or types) usually allow
   4.642 +  to provide mixfix annotations on the spot, which is convenient for default
   4.643 +  notation. Nonetheless, the syntax may be modified later on by declarations
   4.644 +  for explicit notation. This allows to add or delete mixfix annotations for
   4.645 +  of existing logical entities within the current context.
   4.646  
   4.647    @{rail \<open>
   4.648      (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
   4.649 @@ -505,24 +477,22 @@
   4.650      @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
   4.651    \<close>}
   4.652  
   4.653 -  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix
   4.654 -  syntax with an existing type constructor.  The arity of the
   4.655 -  constructor is retrieved from the context.
   4.656 +  \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
   4.657 +  existing type constructor. The arity of the constructor is retrieved from
   4.658 +  the context.
   4.659  
   4.660 -  \<^descr> @{command "no_type_notation"} is similar to @{command
   4.661 -  "type_notation"}, but removes the specified syntax annotation from
   4.662 -  the present context.
   4.663 +  \<^descr> @{command "no_type_notation"} is similar to @{command "type_notation"},
   4.664 +  but removes the specified syntax annotation from the present context.
   4.665  
   4.666 -  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix
   4.667 -  syntax with an existing constant or fixed variable.  The type
   4.668 -  declaration of the given entity is retrieved from the context.
   4.669 +  \<^descr> @{command "notation"}~\<open>c (mx)\<close> associates mixfix syntax with an existing
   4.670 +  constant or fixed variable. The type declaration of the given entity is
   4.671 +  retrieved from the context.
   4.672  
   4.673 -  \<^descr> @{command "no_notation"} is similar to @{command "notation"},
   4.674 -  but removes the specified syntax annotation from the present
   4.675 -  context.
   4.676 +  \<^descr> @{command "no_notation"} is similar to @{command "notation"}, but removes
   4.677 +  the specified syntax annotation from the present context.
   4.678  
   4.679 -  \<^descr> @{command "write"} is similar to @{command "notation"}, but
   4.680 -  works within an Isar proof body.
   4.681 +  \<^descr> @{command "write"} is similar to @{command "notation"}, but works within
   4.682 +  an Isar proof body.
   4.683  \<close>
   4.684  
   4.685  
   4.686 @@ -530,26 +500,24 @@
   4.687  
   4.688  subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
   4.689  
   4.690 -text \<open>The inner lexical syntax vaguely resembles the outer one
   4.691 -  (\secref{sec:outer-lex}), but some details are different.  There are
   4.692 -  two main categories of inner syntax tokens:
   4.693 +text \<open>
   4.694 +  The inner lexical syntax vaguely resembles the outer one
   4.695 +  (\secref{sec:outer-lex}), but some details are different. There are two main
   4.696 +  categories of inner syntax tokens:
   4.697  
   4.698 -  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in
   4.699 -  productions of the given priority grammar (cf.\
   4.700 -  \secref{sec:priority-grammar});
   4.701 +  \<^enum> \<^emph>\<open>delimiters\<close> --- the literal tokens occurring in productions of the given
   4.702 +  priority grammar (cf.\ \secref{sec:priority-grammar});
   4.703  
   4.704    \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
   4.705  
   4.706  
   4.707 -  Delimiters override named tokens and may thus render certain
   4.708 -  identifiers inaccessible.  Sometimes the logical context admits
   4.709 -  alternative ways to refer to the same entity, potentially via
   4.710 -  qualified names.
   4.711 +  Delimiters override named tokens and may thus render certain identifiers
   4.712 +  inaccessible. Sometimes the logical context admits alternative ways to refer
   4.713 +  to the same entity, potentially via qualified names.
   4.714  
   4.715    \<^medskip>
   4.716 -  The categories for named tokens are defined once and for
   4.717 -  all as follows, reusing some categories of the outer token syntax
   4.718 -  (\secref{sec:outer-lex}).
   4.719 +  The categories for named tokens are defined once and for all as follows,
   4.720 +  reusing some categories of the outer token syntax (\secref{sec:outer-lex}).
   4.721  
   4.722    \begin{center}
   4.723    \begin{supertabular}{rcl}
   4.724 @@ -581,32 +549,30 @@
   4.725  
   4.726  subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
   4.727  
   4.728 -text \<open>A context-free grammar consists of a set of \<^emph>\<open>terminal
   4.729 -  symbols\<close>, a set of \<^emph>\<open>nonterminal symbols\<close> and a set of
   4.730 -  \<^emph>\<open>productions\<close>.  Productions have the form \<open>A = \<gamma>\<close>,
   4.731 -  where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of
   4.732 -  terminals and nonterminals.  One designated nonterminal is called
   4.733 -  the \<^emph>\<open>root symbol\<close>.  The language defined by the grammar
   4.734 -  consists of all strings of terminals that can be derived from the
   4.735 -  root symbol by applying productions as rewrite rules.
   4.736 +text \<open>
   4.737 +  A context-free grammar consists of a set of \<^emph>\<open>terminal symbols\<close>, a set of
   4.738 +  \<^emph>\<open>nonterminal symbols\<close> and a set of \<^emph>\<open>productions\<close>. Productions have the
   4.739 +  form \<open>A = \<gamma>\<close>, where \<open>A\<close> is a nonterminal and \<open>\<gamma>\<close> is a string of terminals
   4.740 +  and nonterminals. One designated nonterminal is called the \<^emph>\<open>root symbol\<close>.
   4.741 +  The language defined by the grammar consists of all strings of terminals
   4.742 +  that can be derived from the root symbol by applying productions as rewrite
   4.743 +  rules.
   4.744  
   4.745 -  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority
   4.746 -  grammar\<close>.  Each nonterminal is decorated by an integer priority:
   4.747 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  In a derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten
   4.748 -  using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only if \<open>p \<le> q\<close>.  Any
   4.749 -  priority grammar can be translated into a normal context-free
   4.750 -  grammar by introducing new nonterminals and productions.
   4.751 +  The standard Isabelle parser for inner syntax uses a \<^emph>\<open>priority grammar\<close>.
   4.752 +  Each nonterminal is decorated by an integer priority: \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>. In a
   4.753 +  derivation, \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> may be rewritten using a production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> only
   4.754 +  if \<open>p \<le> q\<close>. Any priority grammar can be translated into a normal
   4.755 +  context-free grammar by introducing new nonterminals and productions.
   4.756  
   4.757    \<^medskip>
   4.758 -  Formally, a set of context free productions \<open>G\<close>
   4.759 -  induces a derivation relation \<open>\<longrightarrow>\<^sub>G\<close> as follows.  Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or nonterminal symbols.
   4.760 -  Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
   4.761 +  Formally, a set of context free productions \<open>G\<close> induces a derivation
   4.762 +  relation \<open>\<longrightarrow>\<^sub>G\<close> as follows. Let \<open>\<alpha>\<close> and \<open>\<beta>\<close> denote strings of terminal or
   4.763 +  nonterminal symbols. Then \<open>\<alpha> A\<^sup>(\<^sup>p\<^sup>) \<beta> \<longrightarrow>\<^sub>G \<alpha> \<gamma> \<beta>\<close> holds if and only if \<open>G\<close>
   4.764    contains some production \<open>A\<^sup>(\<^sup>q\<^sup>) = \<gamma>\<close> for \<open>p \<le> q\<close>.
   4.765  
   4.766    \<^medskip>
   4.767 -  The following grammar for arithmetic expressions
   4.768 -  demonstrates how binding power and associativity of operators can be
   4.769 -  enforced by priorities.
   4.770 +  The following grammar for arithmetic expressions demonstrates how binding
   4.771 +  power and associativity of operators can be enforced by priorities.
   4.772  
   4.773    \begin{center}
   4.774    \begin{tabular}{rclr}
   4.775 @@ -617,28 +583,25 @@
   4.776    \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>=\<close> & \<^verbatim>\<open>-\<close> \<open>A\<^sup>(\<^sup>3\<^sup>)\<close> \\
   4.777    \end{tabular}
   4.778    \end{center}
   4.779 -  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds
   4.780 -  tighter than \<^verbatim>\<open>*\<close>, which binds tighter than \<^verbatim>\<open>+\<close>.
   4.781 -  Furthermore \<^verbatim>\<open>+\<close> associates to the left and
   4.782 -  \<^verbatim>\<open>*\<close> to the right.
   4.783 +  The choice of priorities determines that \<^verbatim>\<open>-\<close> binds tighter than \<^verbatim>\<open>*\<close>, which
   4.784 +  binds tighter than \<^verbatim>\<open>+\<close>. Furthermore \<^verbatim>\<open>+\<close> associates to the left and \<^verbatim>\<open>*\<close> to
   4.785 +  the right.
   4.786  
   4.787    \<^medskip>
   4.788    For clarity, grammars obey these conventions:
   4.789  
   4.790 -  \<^item> All priorities must lie between 0 and 1000.
   4.791 +    \<^item> All priorities must lie between 0 and 1000.
   4.792  
   4.793 -  \<^item> Priority 0 on the right-hand side and priority 1000 on the
   4.794 -  left-hand side may be omitted.
   4.795 +    \<^item> Priority 0 on the right-hand side and priority 1000 on the left-hand
   4.796 +    side may be omitted.
   4.797  
   4.798 -  \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha>
   4.799 -  (p)\<close>, i.e.\ the priority of the left-hand side actually appears in
   4.800 -  a column on the far right.
   4.801 +    \<^item> The production \<open>A\<^sup>(\<^sup>p\<^sup>) = \<alpha>\<close> is written as \<open>A = \<alpha> (p)\<close>, i.e.\ the
   4.802 +    priority of the left-hand side actually appears in a column on the far
   4.803 +    right.
   4.804  
   4.805 -  \<^item> Alternatives are separated by \<open>|\<close>.
   4.806 +    \<^item> Alternatives are separated by \<open>|\<close>.
   4.807  
   4.808 -  \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal
   4.809 -  but obvious way.
   4.810 -
   4.811 +    \<^item> Repetition is indicated by dots \<open>(\<dots>)\<close> in an informal but obvious way.
   4.812  
   4.813    Using these conventions, the example grammar specification above
   4.814    takes the form:
   4.815 @@ -656,8 +619,9 @@
   4.816  
   4.817  subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
   4.818  
   4.819 -text \<open>The priority grammar of the \<open>Pure\<close> theory is defined
   4.820 -  approximately like this:
   4.821 +text \<open>
   4.822 +  The priority grammar of the \<open>Pure\<close> theory is defined approximately like
   4.823 +  this:
   4.824  
   4.825    \begin{center}
   4.826    \begin{supertabular}{rclr}
   4.827 @@ -692,7 +656,6 @@
   4.828      & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
   4.829      & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
   4.830      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
   4.831 -    & \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
   4.832      & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
   4.833      & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
   4.834      & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<equiv>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<^verbatim>\<open>&&&\<close> \\
   4.835 @@ -729,55 +692,54 @@
   4.836    \end{center}
   4.837  
   4.838    \<^medskip>
   4.839 -  Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>;
   4.840 -  see also \secref{sec:inner-lex} for further token categories of the
   4.841 -  inner syntax.  The meaning of the nonterminals defined by the above
   4.842 -  grammar is as follows:
   4.843 +  Here literal terminals are printed \<^verbatim>\<open>verbatim\<close>; see also
   4.844 +  \secref{sec:inner-lex} for further token categories of the inner syntax. The
   4.845 +  meaning of the nonterminals defined by the above grammar is as follows:
   4.846  
   4.847    \<^descr> @{syntax_ref (inner) any} denotes any term.
   4.848  
   4.849 -  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions,
   4.850 -  which are terms of type @{typ prop}.  The syntax of such formulae of
   4.851 -  the meta-logic is carefully distinguished from usual conventions for
   4.852 -  object-logics.  In particular, plain \<open>\<lambda>\<close>-term notation is
   4.853 -  \<^emph>\<open>not\<close> recognized as @{syntax (inner) prop}.
   4.854 +  \<^descr> @{syntax_ref (inner) prop} denotes meta-level propositions, which are
   4.855 +  terms of type @{typ prop}. The syntax of such formulae of the meta-logic is
   4.856 +  carefully distinguished from usual conventions for object-logics. In
   4.857 +  particular, plain \<open>\<lambda>\<close>-term notation is \<^emph>\<open>not\<close> recognized as @{syntax (inner)
   4.858 +  prop}.
   4.859  
   4.860 -  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which
   4.861 -  are embedded into regular @{syntax (inner) prop} by means of an
   4.862 -  explicit \<^verbatim>\<open>PROP\<close> token.
   4.863 +  \<^descr> @{syntax_ref (inner) aprop} denotes atomic propositions, which are
   4.864 +  embedded into regular @{syntax (inner) prop} by means of an explicit \<^verbatim>\<open>PROP\<close>
   4.865 +  token.
   4.866  
   4.867 -  Terms of type @{typ prop} with non-constant head, e.g.\ a plain
   4.868 -  variable, are printed in this form.  Constants that yield type @{typ
   4.869 -  prop} are expected to provide their own concrete syntax; otherwise
   4.870 -  the printed version will appear like @{syntax (inner) logic} and
   4.871 -  cannot be parsed again as @{syntax (inner) prop}.
   4.872 +  Terms of type @{typ prop} with non-constant head, e.g.\ a plain variable,
   4.873 +  are printed in this form. Constants that yield type @{typ prop} are expected
   4.874 +  to provide their own concrete syntax; otherwise the printed version will
   4.875 +  appear like @{syntax (inner) logic} and cannot be parsed again as @{syntax
   4.876 +  (inner) prop}.
   4.877  
   4.878 -  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a
   4.879 -  logical type, excluding type @{typ prop}.  This is the main
   4.880 -  syntactic category of object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables, abstraction, application), plus
   4.881 -  anything defined by the user.
   4.882 +  \<^descr> @{syntax_ref (inner) logic} denotes arbitrary terms of a logical type,
   4.883 +  excluding type @{typ prop}. This is the main syntactic category of
   4.884 +  object-logic entities, covering plain \<open>\<lambda>\<close>-term notation (variables,
   4.885 +  abstraction, application), plus anything defined by the user.
   4.886  
   4.887 -  When specifying notation for logical entities, all logical types
   4.888 -  (excluding @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category
   4.889 -  of @{syntax (inner) logic}.
   4.890 +  When specifying notation for logical entities, all logical types (excluding
   4.891 +  @{typ prop}) are \<^emph>\<open>collapsed\<close> to this single category of @{syntax (inner)
   4.892 +  logic}.
   4.893  
   4.894 -  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for
   4.895 -  indexed syntax.  If omitted, it refers to the first @{keyword_ref
   4.896 -  "structure"} variable in the context.  The special dummy ``\<open>\<index>\<close>'' serves as pattern variable in mixfix annotations that
   4.897 -  introduce indexed notation.
   4.898 +  \<^descr> @{syntax_ref (inner) index} denotes an optional index term for indexed
   4.899 +  syntax. If omitted, it refers to the first @{keyword_ref "structure"}
   4.900 +  variable in the context. The special dummy ``\<open>\<index>\<close>'' serves as pattern
   4.901 +  variable in mixfix annotations that introduce indexed notation.
   4.902  
   4.903 -  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly
   4.904 -  constrained by types.
   4.905 +  \<^descr> @{syntax_ref (inner) idt} denotes identifiers, possibly constrained by
   4.906 +  types.
   4.907  
   4.908 -  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref
   4.909 -  (inner) idt}.  This is the most basic category for variables in
   4.910 -  iterated binders, such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
   4.911 +  \<^descr> @{syntax_ref (inner) idts} denotes a sequence of @{syntax_ref (inner)
   4.912 +  idt}. This is the most basic category for variables in iterated binders,
   4.913 +  such as \<open>\<lambda>\<close> or \<open>\<And>\<close>.
   4.914  
   4.915 -  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns}
   4.916 -  denote patterns for abstraction, cases bindings etc.  In Pure, these
   4.917 -  categories start as a merely copy of @{syntax (inner) idt} and
   4.918 -  @{syntax (inner) idts}, respectively.  Object-logics may add
   4.919 -  additional productions for binding forms.
   4.920 +  \<^descr> @{syntax_ref (inner) pttrn} and @{syntax_ref (inner) pttrns} denote
   4.921 +  patterns for abstraction, cases bindings etc. In Pure, these categories
   4.922 +  start as a merely copy of @{syntax (inner) idt} and @{syntax (inner) idts},
   4.923 +  respectively. Object-logics may add additional productions for binding
   4.924 +  forms.
   4.925  
   4.926    \<^descr> @{syntax_ref (inner) type} denotes types of the meta-logic.
   4.927  
   4.928 @@ -786,58 +748,52 @@
   4.929  
   4.930    Here are some further explanations of certain syntax features.
   4.931  
   4.932 -  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is
   4.933 -  parsed as \<open>x :: (nat y)\<close>, treating \<open>y\<close> like a type
   4.934 -  constructor applied to \<open>nat\<close>.  To avoid this interpretation,
   4.935 -  write \<open>(x :: nat) y\<close> with explicit parentheses.
   4.936 +  \<^item> In @{syntax (inner) idts}, note that \<open>x :: nat y\<close> is parsed as \<open>x :: (nat
   4.937 +  y)\<close>, treating \<open>y\<close> like a type constructor applied to \<open>nat\<close>. To avoid this
   4.938 +  interpretation, write \<open>(x :: nat) y\<close> with explicit parentheses.
   4.939  
   4.940 -  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x ::
   4.941 -  (nat y :: nat)\<close>.  The correct form is \<open>(x :: nat) (y ::
   4.942 -  nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is last in the
   4.943 -  sequence of identifiers.
   4.944 +  \<^item> Similarly, \<open>x :: nat y :: nat\<close> is parsed as \<open>x :: (nat y :: nat)\<close>. The
   4.945 +  correct form is \<open>(x :: nat) (y :: nat)\<close>, or \<open>(x :: nat) y :: nat\<close> if \<open>y\<close> is
   4.946 +  last in the sequence of identifiers.
   4.947  
   4.948 -  \<^item> Type constraints for terms bind very weakly.  For example,
   4.949 -  \<open>x < y :: nat\<close> is normally parsed as \<open>(x < y) ::
   4.950 -  nat\<close>, unless \<open><\<close> has a very low priority, in which case the
   4.951 -  input is likely to be ambiguous.  The correct form is \<open>x < (y
   4.952 -  :: nat)\<close>.
   4.953 +  \<^item> Type constraints for terms bind very weakly. For example, \<open>x < y :: nat\<close>
   4.954 +  is normally parsed as \<open>(x < y) :: nat\<close>, unless \<open><\<close> has a very low priority,
   4.955 +  in which case the input is likely to be ambiguous. The correct form is \<open>x <
   4.956 +  (y :: nat)\<close>.
   4.957  
   4.958    \<^item> Dummy variables (written as underscore) may occur in different
   4.959    roles.
   4.960  
   4.961 -    \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an
   4.962 -    anonymous inference parameter, which is filled-in according to the
   4.963 -    most general type produced by the type-checking phase.
   4.964 +    \<^descr> A type ``\<open>_\<close>'' or ``\<open>_ :: sort\<close>'' acts like an anonymous inference
   4.965 +    parameter, which is filled-in according to the most general type produced
   4.966 +    by the type-checking phase.
   4.967  
   4.968 -    \<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where
   4.969 -    the body does not refer to the binding introduced here.  As in the
   4.970 -    term @{term "\<lambda>x _. x"}, which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
   4.971 +    \<^descr> A bound ``\<open>_\<close>'' refers to a vacuous abstraction, where the body does not
   4.972 +    refer to the binding introduced here. As in the term @{term "\<lambda>x _. x"},
   4.973 +    which is \<open>\<alpha>\<close>-equivalent to \<open>\<lambda>x y. x\<close>.
   4.974  
   4.975 -    \<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding.
   4.976 -    Higher definitional packages usually allow forms like \<open>f x _
   4.977 -    = x\<close>.
   4.978 +    \<^descr> A free ``\<open>_\<close>'' refers to an implicit outer binding. Higher definitional
   4.979 +    packages usually allow forms like \<open>f x _ = x\<close>.
   4.980  
   4.981 -    \<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see
   4.982 -    \secref{sec:term-decls}) refers to an anonymous variable that is
   4.983 -    implicitly abstracted over its context of locally bound variables.
   4.984 -    For example, this allows pattern matching of \<open>{x. f x = g
   4.985 -    x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
   4.986 +    \<^descr> A schematic ``\<open>_\<close>'' (within a term pattern, see \secref{sec:term-decls})
   4.987 +    refers to an anonymous variable that is implicitly abstracted over its
   4.988 +    context of locally bound variables. For example, this allows pattern
   4.989 +    matching of \<open>{x. f x = g x}\<close> against \<open>{x. _ = _}\<close>, or even \<open>{_. _ = _}\<close> by
   4.990      using both bound and schematic dummies.
   4.991  
   4.992 -  \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also
   4.993 -  written as ellipsis symbol \<^verbatim>\<open>\<dots>\<close>.  In both cases this
   4.994 -  refers to a special schematic variable, which is bound in the
   4.995 -  context.  This special term abbreviation works nicely with
   4.996 +  \<^descr> The three literal dots ``\<^verbatim>\<open>...\<close>'' may be also written as ellipsis symbol
   4.997 +  \<^verbatim>\<open>\<dots>\<close>. In both cases this refers to a special schematic variable, which is
   4.998 +  bound in the context. This special term abbreviation works nicely with
   4.999    calculational reasoning (\secref{sec:calculation}).
  4.1000  
  4.1001 -  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated
  4.1002 -  as constant term, and passed through the parse tree in fully
  4.1003 -  internalized form.  This is particularly relevant for translation
  4.1004 -  rules (\secref{sec:syn-trans}), notably on the RHS.
  4.1005 +  \<^descr> \<^verbatim>\<open>CONST\<close> ensures that the given identifier is treated as constant term,
  4.1006 +  and passed through the parse tree in fully internalized form. This is
  4.1007 +  particularly relevant for translation rules (\secref{sec:syn-trans}),
  4.1008 +  notably on the RHS.
  4.1009  
  4.1010 -  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but
  4.1011 -  retains the constant name as given.  This is only relevant to
  4.1012 -  translation rules (\secref{sec:syn-trans}), notably on the LHS.
  4.1013 +  \<^descr> \<^verbatim>\<open>XCONST\<close> is similar to \<^verbatim>\<open>CONST\<close>, but retains the constant name as given.
  4.1014 +  This is only relevant to translation rules (\secref{sec:syn-trans}), notably
  4.1015 +  on the LHS.
  4.1016  \<close>
  4.1017  
  4.1018  
  4.1019 @@ -848,46 +804,45 @@
  4.1020      @{command_def "print_syntax"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  4.1021    \end{matharray}
  4.1022  
  4.1023 -  \<^descr> @{command "print_syntax"} prints the inner syntax of the
  4.1024 -  current context.  The output can be quite large; the most important
  4.1025 -  sections are explained below.
  4.1026 +  \<^descr> @{command "print_syntax"} prints the inner syntax of the current context.
  4.1027 +  The output can be quite large; the most important sections are explained
  4.1028 +  below.
  4.1029  
  4.1030 -    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token
  4.1031 -    language; see \secref{sec:inner-lex}.
  4.1032 -
  4.1033 -    \<^descr> \<open>prods\<close> lists the productions of the underlying
  4.1034 -    priority grammar; see \secref{sec:priority-grammar}.
  4.1035 +    \<^descr> \<open>lexicon\<close> lists the delimiters of the inner token language; see
  4.1036 +    \secref{sec:inner-lex}.
  4.1037  
  4.1038 -    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters are quoted.  Many productions have an extra
  4.1039 -    \<open>\<dots> => name\<close>.  These names later become the heads of parse
  4.1040 -    trees; they also guide the pretty printer.
  4.1041 +    \<^descr> \<open>prods\<close> lists the productions of the underlying priority grammar; see
  4.1042 +    \secref{sec:priority-grammar}.
  4.1043  
  4.1044 -    Productions without such parse tree names are called \<^emph>\<open>copy
  4.1045 -    productions\<close>.  Their right-hand side must have exactly one
  4.1046 -    nonterminal symbol (or named token).  The parser does not create a
  4.1047 -    new parse tree node for copy productions, but simply returns the
  4.1048 -    parse tree of the right-hand symbol.
  4.1049 +    The nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is rendered in plain text as \<open>A[p]\<close>; delimiters
  4.1050 +    are quoted. Many productions have an extra \<open>\<dots> => name\<close>. These names later
  4.1051 +    become the heads of parse trees; they also guide the pretty printer.
  4.1052 +
  4.1053 +    Productions without such parse tree names are called \<^emph>\<open>copy productions\<close>.
  4.1054 +    Their right-hand side must have exactly one nonterminal symbol (or named
  4.1055 +    token). The parser does not create a new parse tree node for copy
  4.1056 +    productions, but simply returns the parse tree of the right-hand symbol.
  4.1057  
  4.1058      If the right-hand side of a copy production consists of a single
  4.1059      nonterminal without any delimiters, then it is called a \<^emph>\<open>chain
  4.1060 -    production\<close>.  Chain productions act as abbreviations: conceptually,
  4.1061 -    they are removed from the grammar by adding new productions.
  4.1062 -    Priority information attached to chain productions is ignored; only
  4.1063 -    the dummy value \<open>-1\<close> is displayed.
  4.1064 +    production\<close>. Chain productions act as abbreviations: conceptually, they
  4.1065 +    are removed from the grammar by adding new productions. Priority
  4.1066 +    information attached to chain productions is ignored; only the dummy value
  4.1067 +    \<open>-1\<close> is displayed.
  4.1068  
  4.1069 -    \<^descr> \<open>print modes\<close> lists the alternative print modes
  4.1070 -    provided by this grammar; see \secref{sec:print-modes}.
  4.1071 +    \<^descr> \<open>print modes\<close> lists the alternative print modes provided by this
  4.1072 +    grammar; see \secref{sec:print-modes}.
  4.1073  
  4.1074 -    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to
  4.1075 -    syntax translations (macros); see \secref{sec:syn-trans}.
  4.1076 +    \<^descr> \<open>parse_rules\<close> and \<open>print_rules\<close> relate to syntax translations (macros);
  4.1077 +    see \secref{sec:syn-trans}.
  4.1078  
  4.1079 -    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of constants that invoke
  4.1080 -    translation functions for abstract syntax trees, which are only
  4.1081 -    required in very special situations; see \secref{sec:tr-funs}.
  4.1082 +    \<^descr> \<open>parse_ast_translation\<close> and \<open>print_ast_translation\<close> list sets of
  4.1083 +    constants that invoke translation functions for abstract syntax trees,
  4.1084 +    which are only required in very special situations; see
  4.1085 +    \secref{sec:tr-funs}.
  4.1086  
  4.1087 -    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close>
  4.1088 -    list the sets of constants that invoke regular translation
  4.1089 -    functions; see \secref{sec:tr-funs}.
  4.1090 +    \<^descr> \<open>parse_translation\<close> and \<open>print_translation\<close> list the sets of constants
  4.1091 +    that invoke regular translation functions; see \secref{sec:tr-funs}.
  4.1092  \<close>
  4.1093  
  4.1094  
  4.1095 @@ -899,37 +854,36 @@
  4.1096      @{attribute_def syntax_ambiguity_limit} & : & \<open>attribute\<close> & default \<open>10\<close> \\
  4.1097    \end{tabular}
  4.1098  
  4.1099 -  Depending on the grammar and the given input, parsing may be
  4.1100 -  ambiguous.  Isabelle lets the Earley parser enumerate all possible
  4.1101 -  parse trees, and then tries to make the best out of the situation.
  4.1102 -  Terms that cannot be type-checked are filtered out, which often
  4.1103 -  leads to a unique result in the end.  Unlike regular type
  4.1104 -  reconstruction, which is applied to the whole collection of input
  4.1105 -  terms simultaneously, the filtering stage only treats each given
  4.1106 -  term in isolation.  Filtering is also not attempted for individual
  4.1107 +  Depending on the grammar and the given input, parsing may be ambiguous.
  4.1108 +  Isabelle lets the Earley parser enumerate all possible parse trees, and then
  4.1109 +  tries to make the best out of the situation. Terms that cannot be
  4.1110 +  type-checked are filtered out, which often leads to a unique result in the
  4.1111 +  end. Unlike regular type reconstruction, which is applied to the whole
  4.1112 +  collection of input terms simultaneously, the filtering stage only treats
  4.1113 +  each given term in isolation. Filtering is also not attempted for individual
  4.1114    types or raw ASTs (as required for @{command translations}).
  4.1115  
  4.1116 -  Certain warning or error messages are printed, depending on the
  4.1117 -  situation and the given configuration options.  Parsing ultimately
  4.1118 -  fails, if multiple results remain after the filtering phase.
  4.1119 +  Certain warning or error messages are printed, depending on the situation
  4.1120 +  and the given configuration options. Parsing ultimately fails, if multiple
  4.1121 +  results remain after the filtering phase.
  4.1122  
  4.1123 -  \<^descr> @{attribute syntax_ambiguity_warning} controls output of
  4.1124 -  explicit warning messages about syntax ambiguity.
  4.1125 +  \<^descr> @{attribute syntax_ambiguity_warning} controls output of explicit warning
  4.1126 +  messages about syntax ambiguity.
  4.1127  
  4.1128 -  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of
  4.1129 -  resulting parse trees that are shown as part of the printed message
  4.1130 -  in case of an ambiguity.
  4.1131 +  \<^descr> @{attribute syntax_ambiguity_limit} determines the number of resulting
  4.1132 +  parse trees that are shown as part of the printed message in case of an
  4.1133 +  ambiguity.
  4.1134  \<close>
  4.1135  
  4.1136  
  4.1137  section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
  4.1138  
  4.1139 -text \<open>The inner syntax engine of Isabelle provides separate
  4.1140 -  mechanisms to transform parse trees either via rewrite systems on
  4.1141 -  first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
  4.1142 -  or syntactic \<open>\<lambda>\<close>-terms (\secref{sec:tr-funs}).  This works
  4.1143 -  both for parsing and printing, as outlined in
  4.1144 -  \figref{fig:parse-print}.
  4.1145 +text \<open>
  4.1146 +  The inner syntax engine of Isabelle provides separate mechanisms to
  4.1147 +  transform parse trees either via rewrite systems on first-order ASTs
  4.1148 +  (\secref{sec:syn-trans}), or ML functions on ASTs or syntactic \<open>\<lambda>\<close>-terms
  4.1149 +  (\secref{sec:tr-funs}). This works both for parsing and printing, as
  4.1150 +  outlined in \figref{fig:parse-print}.
  4.1151  
  4.1152    \begin{figure}[htbp]
  4.1153    \begin{center}
  4.1154 @@ -954,137 +908,129 @@
  4.1155    \caption{Parsing and printing with translations}\label{fig:parse-print}
  4.1156    \end{figure}
  4.1157  
  4.1158 -  These intermediate syntax tree formats eventually lead to a pre-term
  4.1159 -  with all names and binding scopes resolved, but most type
  4.1160 -  information still missing.  Explicit type constraints might be given by
  4.1161 -  the user, or implicit position information by the system --- both
  4.1162 -  need to be passed-through carefully by syntax transformations.
  4.1163 +  These intermediate syntax tree formats eventually lead to a pre-term with
  4.1164 +  all names and binding scopes resolved, but most type information still
  4.1165 +  missing. Explicit type constraints might be given by the user, or implicit
  4.1166 +  position information by the system --- both need to be passed-through
  4.1167 +  carefully by syntax transformations.
  4.1168  
  4.1169 -  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and
  4.1170 -  \<^emph>\<open>uncheck\<close> phases that are intertwined with type-inference (see
  4.1171 -  also @{cite "isabelle-implementation"}).  The latter allows to operate
  4.1172 -  on higher-order abstract syntax with proper binding and type
  4.1173 -  information already available.
  4.1174 +  Pre-terms are further processed by the so-called \<^emph>\<open>check\<close> and \<^emph>\<open>uncheck\<close>
  4.1175 +  phases that are intertwined with type-inference (see also @{cite
  4.1176 +  "isabelle-implementation"}). The latter allows to operate on higher-order
  4.1177 +  abstract syntax with proper binding and type information already available.
  4.1178  
  4.1179 -  As a rule of thumb, anything that manipulates bindings of variables
  4.1180 -  or constants needs to be implemented as syntax transformation (see
  4.1181 -  below).  Anything else is better done via check/uncheck: a prominent
  4.1182 -  example application is the @{command abbreviation} concept of
  4.1183 -  Isabelle/Pure.\<close>
  4.1184 +  As a rule of thumb, anything that manipulates bindings of variables or
  4.1185 +  constants needs to be implemented as syntax transformation (see below).
  4.1186 +  Anything else is better done via check/uncheck: a prominent example
  4.1187 +  application is the @{command abbreviation} concept of Isabelle/Pure.
  4.1188 +\<close>
  4.1189  
  4.1190  
  4.1191  subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
  4.1192  
  4.1193 -text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
  4.1194 -  intermediate AST format that is used for syntax rewriting
  4.1195 -  (\secref{sec:syn-trans}).  It is defined in ML as follows:
  4.1196 +text \<open>
  4.1197 +  The ML datatype @{ML_type Ast.ast} explicitly represents the intermediate
  4.1198 +  AST format that is used for syntax rewriting (\secref{sec:syn-trans}). It is
  4.1199 +  defined in ML as follows:
  4.1200    @{verbatim [display]
  4.1201  \<open>datatype ast =
  4.1202    Constant of string |
  4.1203    Variable of string |
  4.1204    Appl of ast list\<close>}
  4.1205  
  4.1206 -  An AST is either an atom (constant or variable) or a list of (at
  4.1207 -  least two) subtrees.  Occasional diagnostic output of ASTs uses
  4.1208 -  notation that resembles S-expression of LISP.  Constant atoms are
  4.1209 -  shown as quoted strings, variable atoms as non-quoted strings and
  4.1210 -  applications as a parenthesized list of subtrees.  For example, the
  4.1211 -  AST
  4.1212 +  An AST is either an atom (constant or variable) or a list of (at least two)
  4.1213 +  subtrees. Occasional diagnostic output of ASTs uses notation that resembles
  4.1214 +  S-expression of LISP. Constant atoms are shown as quoted strings, variable
  4.1215 +  atoms as non-quoted strings and applications as a parenthesized list of
  4.1216 +  subtrees. For example, the AST
  4.1217    @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
  4.1218 -  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>.  Note that
  4.1219 -  \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are excluded as ASTs, because
  4.1220 -  they have too few subtrees.
  4.1221 +  is pretty-printed as \<^verbatim>\<open>("_abs" x t)\<close>. Note that \<^verbatim>\<open>()\<close> and \<^verbatim>\<open>(x)\<close> are
  4.1222 +  excluded as ASTs, because they have too few subtrees.
  4.1223  
  4.1224    \<^medskip>
  4.1225 -  AST application is merely a pro-forma mechanism to indicate
  4.1226 -  certain syntactic structures.  Thus \<^verbatim>\<open>(c a b)\<close> could mean
  4.1227 -  either term application or type application, depending on the
  4.1228 -  syntactic context.
  4.1229 +  AST application is merely a pro-forma mechanism to indicate certain
  4.1230 +  syntactic structures. Thus \<^verbatim>\<open>(c a b)\<close> could mean either term application or
  4.1231 +  type application, depending on the syntactic context.
  4.1232  
  4.1233 -  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also
  4.1234 -  possible, but ASTs are definitely first-order: the syntax constant
  4.1235 -  \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close> in any way.
  4.1236 -  Proper bindings are introduced in later stages of the term syntax,
  4.1237 -  where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and
  4.1238 -  occurrences of \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound
  4.1239 -  variables (represented as de-Bruijn indices).
  4.1240 +  Nested application like \<^verbatim>\<open>(("_abs" x t) u)\<close> is also possible, but ASTs are
  4.1241 +  definitely first-order: the syntax constant \<^verbatim>\<open>"_abs"\<close> does not bind the \<^verbatim>\<open>x\<close>
  4.1242 +  in any way. Proper bindings are introduced in later stages of the term
  4.1243 +  syntax, where \<^verbatim>\<open>("_abs" x t)\<close> becomes an @{ML Abs} node and occurrences of
  4.1244 +  \<^verbatim>\<open>x\<close> in \<^verbatim>\<open>t\<close> are replaced by bound variables (represented as de-Bruijn
  4.1245 +  indices).
  4.1246  \<close>
  4.1247  
  4.1248  
  4.1249  subsubsection \<open>AST constants versus variables\<close>
  4.1250  
  4.1251 -text \<open>Depending on the situation --- input syntax, output syntax,
  4.1252 -  translation patterns --- the distinction of atomic ASTs as @{ML
  4.1253 -  Ast.Constant} versus @{ML Ast.Variable} serves slightly different
  4.1254 -  purposes.
  4.1255 +text \<open>
  4.1256 +  Depending on the situation --- input syntax, output syntax, translation
  4.1257 +  patterns --- the distinction of atomic ASTs as @{ML Ast.Constant} versus
  4.1258 +  @{ML Ast.Variable} serves slightly different purposes.
  4.1259  
  4.1260 -  Input syntax of a term such as \<open>f a b = c\<close> does not yet
  4.1261 -  indicate the scopes of atomic entities \<open>f, a, b, c\<close>: they
  4.1262 -  could be global constants or local variables, even bound ones
  4.1263 -  depending on the context of the term.  @{ML Ast.Variable} leaves
  4.1264 -  this choice still open: later syntax layers (or translation
  4.1265 -  functions) may capture such a variable to determine its role
  4.1266 -  specifically, to make it a constant, bound variable, free variable
  4.1267 -  etc.  In contrast, syntax translations that introduce already known
  4.1268 -  constants would rather do it via @{ML Ast.Constant} to prevent
  4.1269 -  accidental re-interpretation later on.
  4.1270 +  Input syntax of a term such as \<open>f a b = c\<close> does not yet indicate the scopes
  4.1271 +  of atomic entities \<open>f, a, b, c\<close>: they could be global constants or local
  4.1272 +  variables, even bound ones depending on the context of the term. @{ML
  4.1273 +  Ast.Variable} leaves this choice still open: later syntax layers (or
  4.1274 +  translation functions) may capture such a variable to determine its role
  4.1275 +  specifically, to make it a constant, bound variable, free variable etc. In
  4.1276 +  contrast, syntax translations that introduce already known constants would
  4.1277 +  rather do it via @{ML Ast.Constant} to prevent accidental re-interpretation
  4.1278 +  later on.
  4.1279  
  4.1280 -  Output syntax turns term constants into @{ML Ast.Constant} and
  4.1281 -  variables (free or schematic) into @{ML Ast.Variable}.  This
  4.1282 -  information is precise when printing fully formal \<open>\<lambda>\<close>-terms.
  4.1283 +  Output syntax turns term constants into @{ML Ast.Constant} and variables
  4.1284 +  (free or schematic) into @{ML Ast.Variable}. This information is precise
  4.1285 +  when printing fully formal \<open>\<lambda>\<close>-terms.
  4.1286  
  4.1287    \<^medskip>
  4.1288 -  AST translation patterns (\secref{sec:syn-trans}) that
  4.1289 -  represent terms cannot distinguish constants and variables
  4.1290 -  syntactically.  Explicit indication of \<open>CONST c\<close> inside the
  4.1291 -  term language is required, unless \<open>c\<close> is known as special
  4.1292 -  \<^emph>\<open>syntax constant\<close> (see also @{command syntax}).  It is also
  4.1293 -  possible to use @{command syntax} declarations (without mixfix
  4.1294 -  annotation) to enforce that certain unqualified names are always
  4.1295 -  treated as constant within the syntax machinery.
  4.1296 +  AST translation patterns (\secref{sec:syn-trans}) that represent terms
  4.1297 +  cannot distinguish constants and variables syntactically. Explicit
  4.1298 +  indication of \<open>CONST c\<close> inside the term language is required, unless \<open>c\<close> is
  4.1299 +  known as special \<^emph>\<open>syntax constant\<close> (see also @{command syntax}). It is also
  4.1300 +  possible to use @{command syntax} declarations (without mixfix annotation)
  4.1301 +  to enforce that certain unqualified names are always treated as constant
  4.1302 +  within the syntax machinery.
  4.1303  
  4.1304 -  The situation is simpler for ASTs that represent types or sorts,
  4.1305 -  since the concrete syntax already distinguishes type variables from
  4.1306 -  type constants (constructors).  So \<open>('a, 'b) foo\<close>
  4.1307 -  corresponds to an AST application of some constant for \<open>foo\<close>
  4.1308 -  and variable arguments for \<open>'a\<close> and \<open>'b\<close>.  Note that
  4.1309 -  the postfix application is merely a feature of the concrete syntax,
  4.1310 -  while in the AST the constructor occurs in head position.\<close>
  4.1311 +  The situation is simpler for ASTs that represent types or sorts, since the
  4.1312 +  concrete syntax already distinguishes type variables from type constants
  4.1313 +  (constructors). So \<open>('a, 'b) foo\<close> corresponds to an AST application of some
  4.1314 +  constant for \<open>foo\<close> and variable arguments for \<open>'a\<close> and \<open>'b\<close>. Note that the
  4.1315 +  postfix application is merely a feature of the concrete syntax, while in the
  4.1316 +  AST the constructor occurs in head position.
  4.1317 +\<close>
  4.1318  
  4.1319  
  4.1320  subsubsection \<open>Authentic syntax names\<close>
  4.1321  
  4.1322 -text \<open>Naming constant entities within ASTs is another delicate
  4.1323 -  issue.  Unqualified names are resolved in the name space tables in
  4.1324 -  the last stage of parsing, after all translations have been applied.
  4.1325 -  Since syntax transformations do not know about this later name
  4.1326 -  resolution, there can be surprises in boundary cases.
  4.1327 +text \<open>
  4.1328 +  Naming constant entities within ASTs is another delicate issue. Unqualified
  4.1329 +  names are resolved in the name space tables in the last stage of parsing,
  4.1330 +  after all translations have been applied. Since syntax transformations do
  4.1331 +  not know about this later name resolution, there can be surprises in
  4.1332 +  boundary cases.
  4.1333  
  4.1334 -  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this
  4.1335 -  problem: the fully-qualified constant name with a special prefix for
  4.1336 -  its formal category (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
  4.1337 -  within the untyped AST format.  Accidental overlap with free or
  4.1338 -  bound variables is excluded as well.  Authentic syntax names work
  4.1339 -  implicitly in the following situations:
  4.1340 +  \<^emph>\<open>Authentic syntax names\<close> for @{ML Ast.Constant} avoid this problem: the
  4.1341 +  fully-qualified constant name with a special prefix for its formal category
  4.1342 +  (\<open>class\<close>, \<open>type\<close>, \<open>const\<close>, \<open>fixed\<close>) represents the information faithfully
  4.1343 +  within the untyped AST format. Accidental overlap with free or bound
  4.1344 +  variables is excluded as well. Authentic syntax names work implicitly in the
  4.1345 +  following situations:
  4.1346  
  4.1347 -  \<^item> Input of term constants (or fixed variables) that are
  4.1348 -  introduced by concrete syntax via @{command notation}: the
  4.1349 -  correspondence of a particular grammar production to some known term
  4.1350 -  entity is preserved.
  4.1351 +    \<^item> Input of term constants (or fixed variables) that are introduced by
  4.1352 +    concrete syntax via @{command notation}: the correspondence of a
  4.1353 +    particular grammar production to some known term entity is preserved.
  4.1354  
  4.1355 -  \<^item> Input of type constants (constructors) and type classes ---
  4.1356 -  thanks to explicit syntactic distinction independently on the
  4.1357 -  context.
  4.1358 +    \<^item> Input of type constants (constructors) and type classes --- thanks to
  4.1359 +    explicit syntactic distinction independently on the context.
  4.1360  
  4.1361 -  \<^item> Output of term constants, type constants, type classes ---
  4.1362 -  this information is already available from the internal term to be
  4.1363 -  printed.
  4.1364 -
  4.1365 +    \<^item> Output of term constants, type constants, type classes --- this
  4.1366 +    information is already available from the internal term to be printed.
  4.1367  
  4.1368 -  In other words, syntax transformations that operate on input terms
  4.1369 -  written as prefix applications are difficult to make robust.
  4.1370 -  Luckily, this case rarely occurs in practice, because syntax forms
  4.1371 -  to be translated usually correspond to some concrete notation.\<close>
  4.1372 +  In other words, syntax transformations that operate on input terms written
  4.1373 +  as prefix applications are difficult to make robust. Luckily, this case
  4.1374 +  rarely occurs in practice, because syntax forms to be translated usually
  4.1375 +  correspond to some concrete notation.
  4.1376 +\<close>
  4.1377  
  4.1378  
  4.1379  subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
  4.1380 @@ -1101,14 +1047,13 @@
  4.1381    \end{tabular}
  4.1382    \<^medskip>
  4.1383  
  4.1384 -  Unlike mixfix notation for existing formal entities
  4.1385 -  (\secref{sec:notation}), raw syntax declarations provide full access
  4.1386 -  to the priority grammar of the inner syntax, without any sanity
  4.1387 -  checks.  This includes additional syntactic categories (via
  4.1388 -  @{command nonterminal}) and free-form grammar productions (via
  4.1389 -  @{command syntax}).  Additional syntax translations (or macros, via
  4.1390 -  @{command translations}) are required to turn resulting parse trees
  4.1391 -  into proper representations of formal entities again.
  4.1392 +  Unlike mixfix notation for existing formal entities (\secref{sec:notation}),
  4.1393 +  raw syntax declarations provide full access to the priority grammar of the
  4.1394 +  inner syntax, without any sanity checks. This includes additional syntactic
  4.1395 +  categories (via @{command nonterminal}) and free-form grammar productions
  4.1396 +  (via @{command syntax}). Additional syntax translations (or macros, via
  4.1397 +  @{command translations}) are required to turn resulting parse trees into
  4.1398 +  proper representations of formal entities again.
  4.1399  
  4.1400    @{rail \<open>
  4.1401      @@{command nonterminal} (@{syntax name} + @'and')
  4.1402 @@ -1126,193 +1071,177 @@
  4.1403      transpat: ('(' @{syntax nameref} ')')? @{syntax string}
  4.1404    \<close>}
  4.1405  
  4.1406 -  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type
  4.1407 -  constructor \<open>c\<close> (without arguments) to act as purely syntactic
  4.1408 -  type: a nonterminal symbol of the inner syntax.
  4.1409 +  \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
  4.1410 +  arguments) to act as purely syntactic type: a nonterminal symbol of the
  4.1411 +  inner syntax.
  4.1412  
  4.1413 -  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the
  4.1414 -  priority grammar and the pretty printer table for the given print
  4.1415 -  mode (default \<^verbatim>\<open>""\<close>). An optional keyword @{keyword_ref
  4.1416 -  "output"} means that only the pretty printer table is affected.
  4.1417 +  \<^descr> @{command "syntax"}~\<open>(mode) c :: \<sigma> (mx)\<close> augments the priority grammar and
  4.1418 +  the pretty printer table for the given print mode (default \<^verbatim>\<open>""\<close>). An
  4.1419 +  optional keyword @{keyword_ref "output"} means that only the pretty printer
  4.1420 +  table is affected.
  4.1421  
  4.1422 -  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx =
  4.1423 -  template ps q\<close> together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and
  4.1424 -  specify a grammar production.  The \<open>template\<close> contains
  4.1425 -  delimiter tokens that surround \<open>n\<close> argument positions
  4.1426 -  (\<^verbatim>\<open>_\<close>).  The latter correspond to nonterminal symbols
  4.1427 -  \<open>A\<^sub>i\<close> derived from the argument types \<open>\<tau>\<^sub>i\<close> as
  4.1428 -  follows:
  4.1429 +  Following \secref{sec:mixfix}, the mixfix annotation \<open>mx = template ps q\<close>
  4.1430 +  together with type \<open>\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close> and specify a grammar production.
  4.1431 +  The \<open>template\<close> contains delimiter tokens that surround \<open>n\<close> argument
  4.1432 +  positions (\<^verbatim>\<open>_\<close>). The latter correspond to nonterminal symbols \<open>A\<^sub>i\<close> derived
  4.1433 +  from the argument types \<open>\<tau>\<^sub>i\<close> as follows:
  4.1434  
  4.1435      \<^item> \<open>prop\<close> if \<open>\<tau>\<^sub>i = prop\<close>
  4.1436  
  4.1437 -    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type
  4.1438 -    constructor \<open>\<kappa> \<noteq> prop\<close>
  4.1439 +    \<^item> \<open>logic\<close> if \<open>\<tau>\<^sub>i = (\<dots>)\<kappa>\<close> for logical type constructor \<open>\<kappa> \<noteq> prop\<close>
  4.1440  
  4.1441      \<^item> \<open>any\<close> if \<open>\<tau>\<^sub>i = \<alpha>\<close> for type variables
  4.1442  
  4.1443 -    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close>
  4.1444 -    (syntactic type constructor)
  4.1445 +    \<^item> \<open>\<kappa>\<close> if \<open>\<tau>\<^sub>i = \<kappa>\<close> for nonterminal \<open>\<kappa>\<close> (syntactic type constructor)
  4.1446  
  4.1447 -  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the
  4.1448 -  given list \<open>ps\<close>; missing priorities default to 0.
  4.1449 +  Each \<open>A\<^sub>i\<close> is decorated by priority \<open>p\<^sub>i\<close> from the given list \<open>ps\<close>; missing
  4.1450 +  priorities default to 0.
  4.1451  
  4.1452 -  The resulting nonterminal of the production is determined similarly
  4.1453 -  from type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
  4.1454 +  The resulting nonterminal of the production is determined similarly from
  4.1455 +  type \<open>\<tau>\<close>, with priority \<open>q\<close> and default 1000.
  4.1456  
  4.1457    \<^medskip>
  4.1458 -  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the argument slots.  The resulting parse tree is
  4.1459 -  composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by using the syntax constant \<open>c\<close> of the syntax declaration.
  4.1460 +  Parsing via this production produces parse trees \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> for the
  4.1461 +  argument slots. The resulting parse tree is composed as \<open>c t\<^sub>1 \<dots> t\<^sub>n\<close>, by
  4.1462 +  using the syntax constant \<open>c\<close> of the syntax declaration.
  4.1463  
  4.1464 -  Such syntactic constants are invented on the spot, without formal
  4.1465 -  check wrt.\ existing declarations.  It is conventional to use plain
  4.1466 -  identifiers prefixed by a single underscore (e.g.\ \<open>_foobar\<close>).  Names should be chosen with care, to avoid clashes
  4.1467 -  with other syntax declarations.
  4.1468 +  Such syntactic constants are invented on the spot, without formal check
  4.1469 +  wrt.\ existing declarations. It is conventional to use plain identifiers
  4.1470 +  prefixed by a single underscore (e.g.\ \<open>_foobar\<close>). Names should be chosen
  4.1471 +  with care, to avoid clashes with other syntax declarations.
  4.1472  
  4.1473    \<^medskip>
  4.1474 -  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty string).
  4.1475 -  It means that the resulting parse tree \<open>t\<close> is copied directly, without any
  4.1476 -  further decoration.
  4.1477 +  The special case of copy production is specified by \<open>c =\<close>~\<^verbatim>\<open>""\<close> (empty
  4.1478 +  string). It means that the resulting parse tree \<open>t\<close> is copied directly,
  4.1479 +  without any further decoration.
  4.1480  
  4.1481 -  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar
  4.1482 -  declarations (and translations) resulting from \<open>decls\<close>, which
  4.1483 -  are interpreted in the same manner as for @{command "syntax"} above.
  4.1484 +  \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and
  4.1485 +  translations) resulting from \<open>decls\<close>, which are interpreted in the same
  4.1486 +  manner as for @{command "syntax"} above.
  4.1487 +
  4.1488 +  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
  4.1489 +  (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
  4.1490 +  theory context maintains two independent lists translation rules: parse
  4.1491 +  rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both
  4.1492 +  can be specified simultaneously as parse~/ print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
  4.1493  
  4.1494 -  \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic
  4.1495 -  translation rules (i.e.\ macros) as first-order rewrite rules on
  4.1496 -  ASTs (\secref{sec:ast}).  The theory context maintains two
  4.1497 -  independent lists translation rules: parse rules (\<^verbatim>\<open>=>\<close>
  4.1498 -  or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>).
  4.1499 -  For convenience, both can be specified simultaneously as parse~/
  4.1500 -  print rules (\<^verbatim>\<open>==\<close> or \<open>\<rightleftharpoons>\<close>).
  4.1501 +  Translation patterns may be prefixed by the syntactic category to be used
  4.1502 +  for parsing; the default is \<open>logic\<close> which means that regular term syntax is
  4.1503 +  used. Both sides of the syntax translation rule undergo parsing and parse
  4.1504 +  AST translations \secref{sec:tr-funs}, in order to perform some fundamental
  4.1505 +  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST translation rules
  4.1506 +  are \<^emph>\<open>not\<close> applied recursively here.
  4.1507  
  4.1508 -  Translation patterns may be prefixed by the syntactic category to be
  4.1509 -  used for parsing; the default is \<open>logic\<close> which means that
  4.1510 -  regular term syntax is used.  Both sides of the syntax translation
  4.1511 -  rule undergo parsing and parse AST translations
  4.1512 -  \secref{sec:tr-funs}, in order to perform some fundamental
  4.1513 -  normalization like \<open>\<lambda>x y. b \<leadsto> \<lambda>x. \<lambda>y. b\<close>, but other AST
  4.1514 -  translation rules are \<^emph>\<open>not\<close> applied recursively here.
  4.1515 -
  4.1516 -  When processing AST patterns, the inner syntax lexer runs in a
  4.1517 -  different mode that allows identifiers to start with underscore.
  4.1518 -  This accommodates the usual naming convention for auxiliary syntax
  4.1519 -  constants --- those that do not have a logical counter part --- by
  4.1520 -  allowing to specify arbitrary AST applications within the term
  4.1521 -  syntax, independently of the corresponding concrete syntax.
  4.1522 +  When processing AST patterns, the inner syntax lexer runs in a different
  4.1523 +  mode that allows identifiers to start with underscore. This accommodates the
  4.1524 +  usual naming convention for auxiliary syntax constants --- those that do not
  4.1525 +  have a logical counter part --- by allowing to specify arbitrary AST
  4.1526 +  applications within the term syntax, independently of the corresponding
  4.1527 +  concrete syntax.
  4.1528  
  4.1529    Atomic ASTs are distinguished as @{ML Ast.Constant} versus @{ML
  4.1530 -  Ast.Variable} as follows: a qualified name or syntax constant
  4.1531 -  declared via @{command syntax}, or parse tree head of concrete
  4.1532 -  notation becomes @{ML Ast.Constant}, anything else @{ML
  4.1533 -  Ast.Variable}.  Note that \<open>CONST\<close> and \<open>XCONST\<close> within
  4.1534 -  the term language (\secref{sec:pure-grammar}) allow to enforce
  4.1535 -  treatment as constants.
  4.1536 +  Ast.Variable} as follows: a qualified name or syntax constant declared via
  4.1537 +  @{command syntax}, or parse tree head of concrete notation becomes @{ML
  4.1538 +  Ast.Constant}, anything else @{ML Ast.Variable}. Note that \<open>CONST\<close> and
  4.1539 +  \<open>XCONST\<close> within the term language (\secref{sec:pure-grammar}) allow to
  4.1540 +  enforce treatment as constants.
  4.1541  
  4.1542 -  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following
  4.1543 -  side-conditions:
  4.1544 +  AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following side-conditions:
  4.1545  
  4.1546 -    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain
  4.1547 -    repeated variables.\<^footnote>\<open>The deeper reason for this is that AST
  4.1548 -    equality is not well-defined: different occurrences of the ``same''
  4.1549 -    AST could be decorated differently by accidental type-constraints or
  4.1550 -    source position information, for example.\<close>
  4.1551 +    \<^item> Rules must be left linear: \<open>lhs\<close> must not contain repeated
  4.1552 +    variables.\<^footnote>\<open>The deeper reason for this is that AST equality is not
  4.1553 +    well-defined: different occurrences of the ``same'' AST could be decorated
  4.1554 +    differently by accidental type-constraints or source position information,
  4.1555 +    for example.\<close>
  4.1556  
  4.1557      \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
  4.1558  
  4.1559 -  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic
  4.1560 -  translation rules, which are interpreted in the same manner as for
  4.1561 -  @{command "translations"} above.
  4.1562 +  \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic translation rules,
  4.1563 +  which are interpreted in the same manner as for @{command "translations"}
  4.1564 +  above.
  4.1565  
  4.1566 -  \<^descr> @{attribute syntax_ast_trace} and @{attribute
  4.1567 -  syntax_ast_stats} control diagnostic output in the AST normalization
  4.1568 -  process, when translation rules are applied to concrete input or
  4.1569 -  output.
  4.1570 +  \<^descr> @{attribute syntax_ast_trace} and @{attribute syntax_ast_stats} control
  4.1571 +  diagnostic output in the AST normalization process, when translation rules
  4.1572 +  are applied to concrete input or output.
  4.1573  
  4.1574  
  4.1575 -  Raw syntax and translations provides a slightly more low-level
  4.1576 -  access to the grammar and the form of resulting parse trees.  It is
  4.1577 -  often possible to avoid this untyped macro mechanism, and use
  4.1578 -  type-safe @{command abbreviation} or @{command notation} instead.
  4.1579 -  Some important situations where @{command syntax} and @{command
  4.1580 -  translations} are really need are as follows:
  4.1581 +  Raw syntax and translations provides a slightly more low-level access to the
  4.1582 +  grammar and the form of resulting parse trees. It is often possible to avoid
  4.1583 +  this untyped macro mechanism, and use type-safe @{command abbreviation} or
  4.1584 +  @{command notation} instead. Some important situations where @{command
  4.1585 +  syntax} and @{command translations} are really need are as follows:
  4.1586  
  4.1587 -  \<^item> Iterated replacement via recursive @{command translations}.
  4.1588 -  For example, consider list enumeration @{term "[a, b, c, d]"} as
  4.1589 -  defined in theory @{theory List} in Isabelle/HOL.
  4.1590 +  \<^item> Iterated replacement via recursive @{command translations}. For example,
  4.1591 +  consider list enumeration @{term "[a, b, c, d]"} as defined in theory
  4.1592 +  @{theory List} in Isabelle/HOL.
  4.1593  
  4.1594 -  \<^item> Change of binding status of variables: anything beyond the
  4.1595 -  built-in @{keyword "binder"} mixfix annotation requires explicit
  4.1596 -  syntax translations.  For example, consider list filter
  4.1597 -  comprehension @{term "[x \<leftarrow> xs . P]"} as defined in theory @{theory
  4.1598 -  List} in Isabelle/HOL.
  4.1599 +  \<^item> Change of binding status of variables: anything beyond the built-in
  4.1600 +  @{keyword "binder"} mixfix annotation requires explicit syntax translations.
  4.1601 +  For example, consider list filter comprehension @{term "[x \<leftarrow> xs . P]"} as
  4.1602 +  defined in theory @{theory List} in Isabelle/HOL.
  4.1603  \<close>
  4.1604  
  4.1605  
  4.1606  subsubsection \<open>Applying translation rules\<close>
  4.1607  
  4.1608 -text \<open>As a term is being parsed or printed, an AST is generated as
  4.1609 -  an intermediate form according to \figref{fig:parse-print}.  The AST
  4.1610 -  is normalized by applying translation rules in the manner of a
  4.1611 -  first-order term rewriting system.  We first examine how a single
  4.1612 -  rule is applied.
  4.1613 +text \<open>
  4.1614 +  As a term is being parsed or printed, an AST is generated as an intermediate
  4.1615 +  form according to \figref{fig:parse-print}. The AST is normalized by
  4.1616 +  applying translation rules in the manner of a first-order term rewriting
  4.1617 +  system. We first examine how a single rule is applied.
  4.1618  
  4.1619 -  Let \<open>t\<close> be the abstract syntax tree to be normalized and
  4.1620 -  \<open>(lhs, rhs)\<close> some translation rule.  A subtree \<open>u\<close>
  4.1621 -  of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
  4.1622 -  object \<open>u\<close>.  A redex matched by \<open>lhs\<close> may be
  4.1623 -  replaced by the corresponding instance of \<open>rhs\<close>, thus
  4.1624 -  \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>.  Matching requires some notion
  4.1625 -  of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves
  4.1626 -  this purpose.
  4.1627 +  Let \<open>t\<close> be the abstract syntax tree to be normalized and \<open>(lhs, rhs)\<close> some
  4.1628 +  translation rule. A subtree \<open>u\<close> of \<open>t\<close> is called \<^emph>\<open>redex\<close> if it is an
  4.1629 +  instance of \<open>lhs\<close>; in this case the pattern \<open>lhs\<close> is said to match the
  4.1630 +  object \<open>u\<close>. A redex matched by \<open>lhs\<close> may be replaced by the corresponding
  4.1631 +  instance of \<open>rhs\<close>, thus \<^emph>\<open>rewriting\<close> the AST \<open>t\<close>. Matching requires some
  4.1632 +  notion of \<^emph>\<open>place-holders\<close> in rule patterns: @{ML Ast.Variable} serves this
  4.1633 +  purpose.
  4.1634  
  4.1635 -  More precisely, the matching of the object \<open>u\<close> against the
  4.1636 -  pattern \<open>lhs\<close> is performed as follows:
  4.1637 +  More precisely, the matching of the object \<open>u\<close> against the pattern \<open>lhs\<close> is
  4.1638 +  performed as follows:
  4.1639  
  4.1640 -  \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML
  4.1641 -  Ast.Constant}~\<open>x\<close> are matched by pattern @{ML
  4.1642 -  Ast.Constant}~\<open>x\<close>.  Thus all atomic ASTs in the object are
  4.1643 -  treated as (potential) constants, and a successful match makes them
  4.1644 -  actual constants even before name space resolution (see also
  4.1645 -  \secref{sec:ast}).
  4.1646 +    \<^item> Objects of the form @{ML Ast.Variable}~\<open>x\<close> or @{ML Ast.Constant}~\<open>x\<close> are
  4.1647 +    matched by pattern @{ML Ast.Constant}~\<open>x\<close>. Thus all atomic ASTs in the
  4.1648 +    object are treated as (potential) constants, and a successful match makes
  4.1649 +    them actual constants even before name space resolution (see also
  4.1650 +    \secref{sec:ast}).
  4.1651  
  4.1652 -  \<^item> Object \<open>u\<close> is matched by pattern @{ML
  4.1653 -  Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to \<open>u\<close>.
  4.1654 +    \<^item> Object \<open>u\<close> is matched by pattern @{ML Ast.Variable}~\<open>x\<close>, binding \<open>x\<close> to
  4.1655 +    \<open>u\<close>.
  4.1656  
  4.1657 -  \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML
  4.1658 -  Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and \<open>ts\<close> have the
  4.1659 -  same length and each corresponding subtree matches.
  4.1660 +    \<^item> Object @{ML Ast.Appl}~\<open>us\<close> is matched by @{ML Ast.Appl}~\<open>ts\<close> if \<open>us\<close> and
  4.1661 +    \<open>ts\<close> have the same length and each corresponding subtree matches.
  4.1662  
  4.1663 -  \<^item> In every other case, matching fails.
  4.1664 +    \<^item> In every other case, matching fails.
  4.1665  
  4.1666 -
  4.1667 -  A successful match yields a substitution that is applied to \<open>rhs\<close>, generating the instance that replaces \<open>u\<close>.
  4.1668 +  A successful match yields a substitution that is applied to \<open>rhs\<close>,
  4.1669 +  generating the instance that replaces \<open>u\<close>.
  4.1670  
  4.1671 -  Normalizing an AST involves repeatedly applying translation rules
  4.1672 -  until none are applicable.  This works yoyo-like: top-down,
  4.1673 -  bottom-up, top-down, etc.  At each subtree position, rules are
  4.1674 -  chosen in order of appearance in the theory definitions.
  4.1675 +  Normalizing an AST involves repeatedly applying translation rules until none
  4.1676 +  are applicable. This works yoyo-like: top-down, bottom-up, top-down, etc. At
  4.1677 +  each subtree position, rules are chosen in order of appearance in the theory
  4.1678 +  definitions.
  4.1679  
  4.1680 -  The configuration options @{attribute syntax_ast_trace} and
  4.1681 -  @{attribute syntax_ast_stats} might help to understand this process
  4.1682 -  and diagnose problems.
  4.1683 +  The configuration options @{attribute syntax_ast_trace} and @{attribute
  4.1684 +  syntax_ast_stats} might help to understand this process and diagnose
  4.1685 +  problems.
  4.1686  
  4.1687    \begin{warn}
  4.1688 -  If syntax translation rules work incorrectly, the output of
  4.1689 -  @{command_ref print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the
  4.1690 -  actual internal forms of AST pattern, without potentially confusing
  4.1691 -  concrete syntax.  Recall that AST constants appear as quoted strings
  4.1692 -  and variables without quotes.
  4.1693 +  If syntax translation rules work incorrectly, the output of @{command_ref
  4.1694 +  print_syntax} with its \<^emph>\<open>rules\<close> sections reveals the actual internal forms
  4.1695 +  of AST pattern, without potentially confusing concrete syntax. Recall that
  4.1696 +  AST constants appear as quoted strings and variables without quotes.
  4.1697    \end{warn}
  4.1698  
  4.1699    \begin{warn}
  4.1700 -  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms
  4.1701 -  will be \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees
  4.1702 -  them.  Thus some abstraction nodes needed for print rules to match
  4.1703 -  may vanish.  For example, \<open>Ball A (\<lambda>x. P x)\<close> would contract
  4.1704 -  to \<open>Ball A P\<close> and the standard print rule would fail to
  4.1705 -  apply.  This problem can be avoided by hand-written ML translation
  4.1706 -  functions (see also \secref{sec:tr-funs}), which is in fact the same
  4.1707 -  mechanism used in built-in @{keyword "binder"} declarations.
  4.1708 +  If @{attribute_ref eta_contract} is set to \<open>true\<close>, terms will be
  4.1709 +  \<open>\<eta>\<close>-contracted \<^emph>\<open>before\<close> the AST rewriter sees them. Thus some abstraction
  4.1710 +  nodes needed for print rules to match may vanish. For example, \<open>Ball A (\<lambda>x.
  4.1711 +  P x)\<close> would contract to \<open>Ball A P\<close> and the standard print rule would fail to
  4.1712 +  apply. This problem can be avoided by hand-written ML translation functions
  4.1713 +  (see also \secref{sec:tr-funs}), which is in fact the same mechanism used in
  4.1714 +  built-in @{keyword "binder"} declarations.
  4.1715    \end{warn}
  4.1716  \<close>
  4.1717  
  4.1718 @@ -1347,10 +1276,9 @@
  4.1719     @@{ML_antiquotation syntax_const}) name
  4.1720    \<close>}
  4.1721  
  4.1722 -  \<^descr> @{command parse_translation} etc. declare syntax translation
  4.1723 -  functions to the theory.  Any of these commands have a single
  4.1724 -  @{syntax text} argument that refers to an ML expression of
  4.1725 -  appropriate type as follows:
  4.1726 +  \<^descr> @{command parse_translation} etc. declare syntax translation functions to
  4.1727 +  the theory. Any of these commands have a single @{syntax text} argument that
  4.1728 +  refers to an ML expression of appropriate type as follows:
  4.1729  
  4.1730    \<^medskip>
  4.1731    {\footnotesize
  4.1732 @@ -1368,110 +1296,108 @@
  4.1733    \end{tabular}}
  4.1734    \<^medskip>
  4.1735  
  4.1736 -  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name of the formal entity involved, and \<open>tr\<close> a function that translates a syntax form \<open>c args\<close> into
  4.1737 -  \<open>tr ctxt args\<close> (depending on the context).  The Isabelle/ML
  4.1738 -  naming convention for parse translations is \<open>c_tr\<close> and for
  4.1739 -  print translations \<open>c_tr'\<close>.
  4.1740 +  The argument list consists of \<open>(c, tr)\<close> pairs, where \<open>c\<close> is the syntax name
  4.1741 +  of the formal entity involved, and \<open>tr\<close> a function that translates a syntax
  4.1742 +  form \<open>c args\<close> into \<open>tr ctxt args\<close> (depending on the context). The
  4.1743 +  Isabelle/ML naming convention for parse translations is \<open>c_tr\<close> and for print
  4.1744 +  translations \<open>c_tr'\<close>.
  4.1745  
  4.1746    The @{command_ref print_syntax} command displays the sets of names
  4.1747 -  associated with the translation functions of a theory under \<open>parse_ast_translation\<close> etc.
  4.1748 +  associated with the translation functions of a theory under
  4.1749 +  \<open>parse_ast_translation\<close> etc.
  4.1750  
  4.1751 -  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>,
  4.1752 -  \<open>@{const_syntax c}\<close> inline the authentic syntax name of the
  4.1753 -  given formal entities into the ML source.  This is the
  4.1754 -  fully-qualified logical name prefixed by a special marker to
  4.1755 -  indicate its kind: thus different logical name spaces are properly
  4.1756 -  distinguished within parse trees.
  4.1757 +  \<^descr> \<open>@{class_syntax c}\<close>, \<open>@{type_syntax c}\<close>, \<open>@{const_syntax c}\<close> inline the
  4.1758 +  authentic syntax name of the given formal entities into the ML source. This
  4.1759 +  is the fully-qualified logical name prefixed by a special marker to indicate
  4.1760 +  its kind: thus different logical name spaces are properly distinguished
  4.1761 +  within parse trees.
  4.1762  
  4.1763 -  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of
  4.1764 -  the given syntax constant, having checked that it has been declared
  4.1765 -  via some @{command syntax} commands within the theory context.  Note
  4.1766 -  that the usual naming convention makes syntax constants start with
  4.1767 -  underscore, to reduce the chance of accidental clashes with other
  4.1768 -  names occurring in parse trees (unqualified constants etc.).
  4.1769 +  \<^descr> \<open>@{const_syntax c}\<close> inlines the name \<open>c\<close> of the given syntax constant,
  4.1770 +  having checked that it has been declared via some @{command syntax} commands
  4.1771 +  within the theory context. Note that the usual naming convention makes
  4.1772 +  syntax constants start with underscore, to reduce the chance of accidental
  4.1773 +  clashes with other names occurring in parse trees (unqualified constants
  4.1774 +  etc.).
  4.1775  \<close>
  4.1776  
  4.1777  
  4.1778  subsubsection \<open>The translation strategy\<close>
  4.1779  
  4.1780 -text \<open>The different kinds of translation functions are invoked during
  4.1781 -  the transformations between parse trees, ASTs and syntactic terms
  4.1782 -  (cf.\ \figref{fig:parse-print}).  Whenever a combination of the form
  4.1783 -  \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close> is encountered, and a translation function
  4.1784 -  \<open>f\<close> of appropriate kind is declared for \<open>c\<close>, the
  4.1785 -  result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close> in ML.
  4.1786 +text \<open>
  4.1787 +  The different kinds of translation functions are invoked during the
  4.1788 +  transformations between parse trees, ASTs and syntactic terms (cf.\
  4.1789 +  \figref{fig:parse-print}). Whenever a combination of the form \<open>c x\<^sub>1 \<dots> x\<^sub>n\<close>
  4.1790 +  is encountered, and a translation function \<open>f\<close> of appropriate kind is
  4.1791 +  declared for \<open>c\<close>, the result is produced by evaluation of \<open>f [x\<^sub>1, \<dots>, x\<^sub>n]\<close>
  4.1792 +  in ML.
  4.1793  
  4.1794 -  For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs.  A
  4.1795 -  combination has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML
  4.1796 -  "Ast.Appl"}~\<open>[\<close>@{ML Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>.
  4.1797 -  For term translations, the arguments are terms and a combination has
  4.1798 -  the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML Const}~\<open>(c, \<tau>)
  4.1799 -  $ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>.  Terms allow more sophisticated transformations
  4.1800 -  than ASTs do, typically involving abstractions and bound
  4.1801 -  variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type
  4.1802 -  \<open>\<tau>\<close> of the constant they are invoked on, although some
  4.1803 -  information might have been suppressed for term output already.
  4.1804 +  For AST translations, the arguments \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> are ASTs. A combination
  4.1805 +  has the form @{ML "Ast.Constant"}~\<open>c\<close> or @{ML "Ast.Appl"}~\<open>[\<close>@{ML
  4.1806 +  Ast.Constant}~\<open>c, x\<^sub>1, \<dots>, x\<^sub>n]\<close>. For term translations, the arguments are
  4.1807 +  terms and a combination has the form @{ML Const}~\<open>(c, \<tau>)\<close> or @{ML
  4.1808 +  Const}~\<open>(c, \<tau>) $ x\<^sub>1 $ \<dots> $ x\<^sub>n\<close>. Terms allow more sophisticated
  4.1809 +  transformations than ASTs do, typically involving abstractions and bound
  4.1810 +  variables. \<^emph>\<open>Typed\<close> print translations may even peek at the type \<open>\<tau>\<close> of the
  4.1811 +  constant they are invoked on, although some information might have been
  4.1812 +  suppressed for term output already.
  4.1813  
  4.1814 -  Regardless of whether they act on ASTs or terms, translation
  4.1815 -  functions called during the parsing process differ from those for
  4.1816 -  printing in their overall behaviour:
  4.1817 +  Regardless of whether they act on ASTs or terms, translation functions
  4.1818 +  called during the parsing process differ from those for printing in their
  4.1819 +  overall behaviour:
  4.1820  
  4.1821 -  \<^descr>[Parse translations] are applied bottom-up.  The arguments are
  4.1822 -  already in translated form.  The translations must not fail;
  4.1823 -  exceptions trigger an error message.  There may be at most one
  4.1824 -  function associated with any syntactic name.
  4.1825 +    \<^descr>[Parse translations] are applied bottom-up. The arguments are already in
  4.1826 +    translated form. The translations must not fail; exceptions trigger an
  4.1827 +    error message. There may be at most one function associated with any
  4.1828 +    syntactic name.
  4.1829  
  4.1830 -  \<^descr>[Print translations] are applied top-down.  They are supplied
  4.1831 -  with arguments that are partly still in internal form.  The result
  4.1832 -  again undergoes translation; therefore a print translation should
  4.1833 -  not introduce as head the very constant that invoked it.  The
  4.1834 -  function may raise exception @{ML Match} to indicate failure; in
  4.1835 -  this event it has no effect.  Multiple functions associated with
  4.1836 -  some syntactic name are tried in the order of declaration in the
  4.1837 -  theory.
  4.1838 +    \<^descr>[Print translations] are applied top-down. They are supplied with
  4.1839 +    arguments that are partly still in internal form. The result again
  4.1840 +    undergoes translation; therefore a print translation should not introduce
  4.1841 +    as head the very constant that invoked it. The function may raise
  4.1842 +    exception @{ML Match} to indicate failure; in this event it has no effect.
  4.1843 +    Multiple functions associated with some syntactic name are tried in the
  4.1844 +    order of declaration in the theory.
  4.1845  
  4.1846 -
  4.1847 -  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and
  4.1848 -  @{ML Const} for terms --- can invoke translation functions.  This
  4.1849 -  means that parse translations can only be associated with parse tree
  4.1850 -  heads of concrete syntax, or syntactic constants introduced via
  4.1851 -  other translations.  For plain identifiers within the term language,
  4.1852 -  the status of constant versus variable is not yet know during
  4.1853 -  parsing.  This is in contrast to print translations, where constants
  4.1854 -  are explicitly known from the given term in its fully internal form.
  4.1855 +  Only constant atoms --- constructor @{ML Ast.Constant} for ASTs and @{ML
  4.1856 +  Const} for terms --- can invoke translation functions. This means that parse
  4.1857 +  translations can only be associated with parse tree heads of concrete
  4.1858 +  syntax, or syntactic constants introduced via other translations. For plain
  4.1859 +  identifiers within the term language, the status of constant versus variable
  4.1860 +  is not yet know during parsing. This is in contrast to print translations,
  4.1861 +  where constants are explicitly known from the given term in its fully
  4.1862 +  internal form.
  4.1863  \<close>
  4.1864  
  4.1865  
  4.1866  subsection \<open>Built-in syntax transformations\<close>
  4.1867  
  4.1868  text \<open>
  4.1869 -  Here are some further details of the main syntax transformation
  4.1870 -  phases of \figref{fig:parse-print}.
  4.1871 +  Here are some further details of the main syntax transformation phases of
  4.1872 +  \figref{fig:parse-print}.
  4.1873  \<close>
  4.1874  
  4.1875  
  4.1876  subsubsection \<open>Transforming parse trees to ASTs\<close>
  4.1877  
  4.1878 -text \<open>The parse tree is the raw output of the parser.  It is
  4.1879 -  transformed into an AST according to some basic scheme that may be
  4.1880 -  augmented by AST translation functions as explained in
  4.1881 -  \secref{sec:tr-funs}.
  4.1882 +text \<open>
  4.1883 +  The parse tree is the raw output of the parser. It is transformed into an
  4.1884 +  AST according to some basic scheme that may be augmented by AST translation
  4.1885 +  functions as explained in \secref{sec:tr-funs}.
  4.1886  
  4.1887    The parse tree is constructed by nesting the right-hand sides of the
  4.1888 -  productions used to recognize the input.  Such parse trees are
  4.1889 -  simply lists of tokens and constituent parse trees, the latter
  4.1890 -  representing the nonterminals of the productions.  Ignoring AST
  4.1891 -  translation functions, parse trees are transformed to ASTs by
  4.1892 -  stripping out delimiters and copy productions, while retaining some
  4.1893 -  source position information from input tokens.
  4.1894 +  productions used to recognize the input. Such parse trees are simply lists
  4.1895 +  of tokens and constituent parse trees, the latter representing the
  4.1896 +  nonterminals of the productions. Ignoring AST translation functions, parse
  4.1897 +  trees are transformed to ASTs by stripping out delimiters and copy
  4.1898 +  productions, while retaining some source position information from input
  4.1899 +  tokens.
  4.1900  
  4.1901 -  The Pure syntax provides predefined AST translations to make the
  4.1902 -  basic \<open>\<lambda>\<close>-term structure more apparent within the
  4.1903 -  (first-order) AST representation, and thus facilitate the use of
  4.1904 -  @{command translations} (see also \secref{sec:syn-trans}).  This
  4.1905 -  covers ordinary term application, type application, nested
  4.1906 -  abstraction, iterated meta implications and function types.  The
  4.1907 -  effect is illustrated on some representative input strings is as
  4.1908 +  The Pure syntax provides predefined AST translations to make the basic
  4.1909 +  \<open>\<lambda>\<close>-term structure more apparent within the (first-order) AST
  4.1910 +  representation, and thus facilitate the use of @{command translations} (see
  4.1911 +  also \secref{sec:syn-trans}). This covers ordinary term application, type
  4.1912 +  application, nested abstraction, iterated meta implications and function
  4.1913 +  types. The effect is illustrated on some representative input strings is as
  4.1914    follows:
  4.1915  
  4.1916    \begin{center}
  4.1917 @@ -1489,85 +1415,83 @@
  4.1918    \end{center}
  4.1919  
  4.1920    Note that type and sort constraints may occur in further places ---
  4.1921 -  translations need to be ready to cope with them.  The built-in
  4.1922 -  syntax transformation from parse trees to ASTs insert additional
  4.1923 -  constraints that represent source positions.
  4.1924 +  translations need to be ready to cope with them. The built-in syntax
  4.1925 +  transformation from parse trees to ASTs insert additional constraints that
  4.1926 +  represent source positions.
  4.1927  \<close>
  4.1928  
  4.1929  
  4.1930  subsubsection \<open>Transforming ASTs to terms\<close>
  4.1931  
  4.1932 -text \<open>After application of macros (\secref{sec:syn-trans}), the AST
  4.1933 -  is transformed into a term.  This term still lacks proper type
  4.1934 -  information, but it might contain some constraints consisting of
  4.1935 -  applications with head \<^verbatim>\<open>_constrain\<close>, where the second
  4.1936 -  argument is a type encoded as a pre-term within the syntax.  Type
  4.1937 -  inference later introduces correct types, or indicates type errors
  4.1938 -  in the input.
  4.1939 +text \<open>
  4.1940 +  After application of macros (\secref{sec:syn-trans}), the AST is transformed
  4.1941 +  into a term. This term still lacks proper type information, but it might
  4.1942 +  contain some constraints consisting of applications with head \<^verbatim>\<open>_constrain\<close>,
  4.1943 +  where the second argument is a type encoded as a pre-term within the syntax.
  4.1944 +  Type inference later introduces correct types, or indicates type errors in
  4.1945 +  the input.
  4.1946  
  4.1947 -  Ignoring parse translations, ASTs are transformed to terms by
  4.1948 -  mapping AST constants to term constants, AST variables to term
  4.1949 -  variables or constants (according to the name space), and AST
  4.1950 -  applications to iterated term applications.
  4.1951 +  Ignoring parse translations, ASTs are transformed to terms by mapping AST
  4.1952 +  constants to term constants, AST variables to term variables or constants
  4.1953 +  (according to the name space), and AST applications to iterated term
  4.1954 +  applications.
  4.1955  
  4.1956 -  The outcome is still a first-order term.  Proper abstractions and
  4.1957 -  bound variables are introduced by parse translations associated with
  4.1958 -  certain syntax constants.  Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually
  4.1959 -  becomes a de-Bruijn term \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
  4.1960 +  The outcome is still a first-order term. Proper abstractions and bound
  4.1961 +  variables are introduced by parse translations associated with certain
  4.1962 +  syntax constants. Thus \<^verbatim>\<open>("_abs" x x)\<close> eventually becomes a de-Bruijn term
  4.1963 +  \<^verbatim>\<open>Abs ("x", _, Bound 0)\<close>.
  4.1964  \<close>
  4.1965  
  4.1966  
  4.1967  subsubsection \<open>Printing of terms\<close>
  4.1968  
  4.1969 -text \<open>The output phase is essentially the inverse of the input
  4.1970 -  phase.  Terms are translated via abstract syntax trees into
  4.1971 -  pretty-printed text.
  4.1972 +text \<open>
  4.1973 +  The output phase is essentially the inverse of the input phase. Terms are
  4.1974 +  translated via abstract syntax trees into pretty-printed text.
  4.1975  
  4.1976    Ignoring print translations, the transformation maps term constants,
  4.1977    variables and applications to the corresponding constructs on ASTs.
  4.1978 -  Abstractions are mapped to applications of the special constant
  4.1979 -  \<^verbatim>\<open>_abs\<close> as seen before.  Type constraints are represented
  4.1980 -  via special \<^verbatim>\<open>_constrain\<close> forms, according to various
  4.1981 -  policies of type annotation determined elsewhere.  Sort constraints
  4.1982 -  of type variables are handled in a similar fashion.
  4.1983 +  Abstractions are mapped to applications of the special constant \<^verbatim>\<open>_abs\<close> as
  4.1984 +  seen before. Type constraints are represented via special \<^verbatim>\<open>_constrain\<close>
  4.1985 +  forms, according to various policies of type annotation determined
  4.1986 +  elsewhere. Sort constraints of type variables are handled in a similar
  4.1987 +  fashion.
  4.1988  
  4.1989 -  After application of macros (\secref{sec:syn-trans}), the AST is
  4.1990 -  finally pretty-printed.  The built-in print AST translations reverse
  4.1991 -  the corresponding parse AST translations.
  4.1992 +  After application of macros (\secref{sec:syn-trans}), the AST is finally
  4.1993 +  pretty-printed. The built-in print AST translations reverse the
  4.1994 +  corresponding parse AST translations.
  4.1995  
  4.1996    \<^medskip>
  4.1997    For the actual printing process, the priority grammar
  4.1998 -  (\secref{sec:priority-grammar}) plays a vital role: productions are
  4.1999 -  used as templates for pretty printing, with argument slots stemming
  4.2000 -  from nonterminals, and syntactic sugar stemming from literal tokens.
  4.2001 +  (\secref{sec:priority-grammar}) plays a vital role: productions are used as
  4.2002 +  templates for pretty printing, with argument slots stemming from
  4.2003 +  nonterminals, and syntactic sugar stemming from literal tokens.
  4.2004  
  4.2005 -  Each AST application with constant head \<open>c\<close> and arguments
  4.2006 -  \<open>t\<^sub>1\<close>, \dots, \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is
  4.2007 -  just the constant \<open>c\<close> itself) is printed according to the
  4.2008 -  first grammar production of result name \<open>c\<close>.  The required
  4.2009 -  syntax priority of the argument slot is given by its nonterminal
  4.2010 -  \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.  The argument \<open>t\<^sub>i\<close> that corresponds to the
  4.2011 -  position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed recursively, and then put in
  4.2012 -  parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires this.  The
  4.2013 -  resulting output is concatenated with the syntactic sugar according
  4.2014 -  to the grammar production.
  4.2015 +  Each AST application with constant head \<open>c\<close> and arguments \<open>t\<^sub>1\<close>, \dots,
  4.2016 +  \<open>t\<^sub>n\<close> (for \<open>n = 0\<close> the AST is just the constant \<open>c\<close> itself) is printed
  4.2017 +  according to the first grammar production of result name \<open>c\<close>. The required
  4.2018 +  syntax priority of the argument slot is given by its nonterminal \<open>A\<^sup>(\<^sup>p\<^sup>)\<close>.
  4.2019 +  The argument \<open>t\<^sub>i\<close> that corresponds to the position of \<open>A\<^sup>(\<^sup>p\<^sup>)\<close> is printed
  4.2020 +  recursively, and then put in parentheses \<^emph>\<open>if\<close> its priority \<open>p\<close> requires
  4.2021 +  this. The resulting output is concatenated with the syntactic sugar
  4.2022 +  according to the grammar production.
  4.2023  
  4.2024 -  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than
  4.2025 -  the corresponding production, it is first split into \<open>((c x\<^sub>1
  4.2026 -  \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots> x\<^sub>m)\<close> and then printed recursively as above.
  4.2027 +  If an AST application \<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> has more arguments than the
  4.2028 +  corresponding production, it is first split into \<open>((c x\<^sub>1 \<dots> x\<^sub>n) x\<^sub>n\<^sub>+\<^sub>1 \<dots>
  4.2029 +  x\<^sub>m)\<close> and then printed recursively as above.
  4.2030  
  4.2031 -  Applications with too few arguments or with non-constant head or
  4.2032 -  without a corresponding production are printed in prefix-form like
  4.2033 -  \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for terms.
  4.2034 +  Applications with too few arguments or with non-constant head or without a
  4.2035 +  corresponding production are printed in prefix-form like \<open>f t\<^sub>1 \<dots> t\<^sub>n\<close> for
  4.2036 +  terms.
  4.2037  
  4.2038 -  Multiple productions associated with some name \<open>c\<close> are tried
  4.2039 -  in order of appearance within the grammar.  An occurrence of some
  4.2040 -  AST variable \<open>x\<close> is printed as \<open>x\<close> outright.
  4.2041 +  Multiple productions associated with some name \<open>c\<close> are tried in order of
  4.2042 +  appearance within the grammar. An occurrence of some AST variable \<open>x\<close> is
  4.2043 +  printed as \<open>x\<close> outright.
  4.2044  
  4.2045    \<^medskip>
  4.2046 -  White space is \<^emph>\<open>not\<close> inserted automatically.  If
  4.2047 -  blanks (or breaks) are required to separate tokens, they need to be
  4.2048 -  specified in the mixfix declaration (\secref{sec:mixfix}).
  4.2049 +  White space is \<^emph>\<open>not\<close> inserted automatically. If blanks (or breaks) are
  4.2050 +  required to separate tokens, they need to be specified in the mixfix
  4.2051 +  declaration (\secref{sec:mixfix}).
  4.2052  \<close>
  4.2053  
  4.2054  end
     5.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Jan 08 17:41:04 2016 +0100
     5.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Jan 09 13:31:31 2016 +0100
     5.3 @@ -298,7 +298,7 @@
     5.4    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     5.5        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
     5.6  translations
     5.7 -  "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
     5.8 +  "\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A"
     5.9    -- \<open>Beware of argument permutation!\<close>
    5.10  
    5.11  lemma (in comm_monoid) finprod_empty [simp]: 
     6.1 --- a/src/HOL/Algebra/Ring.thy	Fri Jan 08 17:41:04 2016 +0100
     6.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Jan 09 13:31:31 2016 +0100
     6.3 @@ -38,7 +38,7 @@
     6.4    "_finsum" :: "index => idt => 'a set => 'b => 'b"
     6.5        ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
     6.6  translations
     6.7 -  "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
     6.8 +  "\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (%i. b) A"
     6.9    -- \<open>Beware of argument permutation!\<close>
    6.10  
    6.11  
     7.1 --- a/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Fri Jan 08 17:41:04 2016 +0100
     7.2 +++ b/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Sat Jan 09 13:31:31 2016 +0100
     7.3 @@ -200,23 +200,23 @@
     7.4  lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
     7.5  by (fixrec_simp, cases r, simp_all)
     7.6  
     7.7 -abbreviation apR (infixl "\<diamond>" 70)
     7.8 -  where "a \<diamond> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
     7.9 +abbreviation apR (infixl "\<diamondop>" 70)
    7.10 +  where "a \<diamondop> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
    7.11  
    7.12  text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
    7.13  
    7.14 -lemma R_homomorphism: "Done\<cdot>f \<diamond> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
    7.15 +lemma R_homomorphism: "Done\<cdot>f \<diamondop> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
    7.16    by simp
    7.17  
    7.18 -lemma R_identity: "Done\<cdot>ID \<diamond> r = r"
    7.19 +lemma R_identity: "Done\<cdot>ID \<diamondop> r = r"
    7.20    by (induct r, simp_all add: mapN_mapN eta_cfun)
    7.21  
    7.22 -lemma R_interchange: "r \<diamond> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamond> r"
    7.23 +lemma R_interchange: "r \<diamondop> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamondop> r"
    7.24    by (induct r, simp_all add: mapN_mapN)
    7.25  
    7.26  text {* The associativity rule is the hard one! *}
    7.27  
    7.28 -lemma R_associativity: "Done\<cdot>cfcomp \<diamond> r1 \<diamond> r2 \<diamond> r3 = r1 \<diamond> (r2 \<diamond> r3)"
    7.29 +lemma R_associativity: "Done\<cdot>cfcomp \<diamondop> r1 \<diamondop> r2 \<diamondop> r3 = r1 \<diamondop> (r2 \<diamondop> r3)"
    7.30  proof (induct r1 arbitrary: r2 r3)
    7.31    case (Done x1) thus ?case
    7.32    proof (induct r2 arbitrary: r3)
     8.1 --- a/src/Pure/General/symbol.scala	Fri Jan 08 17:41:04 2016 +0100
     8.2 +++ b/src/Pure/General/symbol.scala	Sat Jan 09 13:31:31 2016 +0100
     8.3 @@ -468,14 +468,14 @@
     8.4      val control_decoded: Set[Symbol] =
     8.5        Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
     8.6  
     8.7 -    val sub_decoded = decode("\\<^sub>")
     8.8 -    val sup_decoded = decode("\\<^sup>")
     8.9 +    val sub_decoded = decode(sub)
    8.10 +    val sup_decoded = decode(sup)
    8.11 +    val bold_decoded = decode(bold)
    8.12 +    val emph_decoded = decode(emph)
    8.13      val bsub_decoded = decode("\\<^bsub>")
    8.14      val esub_decoded = decode("\\<^esub>")
    8.15      val bsup_decoded = decode("\\<^bsup>")
    8.16      val esup_decoded = decode("\\<^esup>")
    8.17 -    val bold_decoded = decode("\\<^bold>")
    8.18 -    val emph_decoded = decode("\\<^emph>")
    8.19    }
    8.20  
    8.21  
    8.22 @@ -557,12 +557,17 @@
    8.23    def is_controllable(sym: Symbol): Boolean =
    8.24      !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) && !is_malformed(sym)
    8.25  
    8.26 +  val sub = "\\<^sub>"
    8.27 +  val sup = "\\<^sup>"
    8.28 +  val bold = "\\<^bold>"
    8.29 +  val emph = "\\<^emph>"
    8.30 +
    8.31    def sub_decoded: Symbol = symbols.sub_decoded
    8.32    def sup_decoded: Symbol = symbols.sup_decoded
    8.33 +  def bold_decoded: Symbol = symbols.bold_decoded
    8.34 +  def emph_decoded: Symbol = symbols.emph_decoded
    8.35    def bsub_decoded: Symbol = symbols.bsub_decoded
    8.36    def esub_decoded: Symbol = symbols.esub_decoded
    8.37    def bsup_decoded: Symbol = symbols.bsup_decoded
    8.38    def esup_decoded: Symbol = symbols.esup_decoded
    8.39 -  def bold_decoded: Symbol = symbols.bold_decoded
    8.40 -  def emph_decoded: Symbol = symbols.emph_decoded
    8.41  }
     9.1 --- a/src/Pure/Isar/token.scala	Fri Jan 08 17:41:04 2016 +0100
     9.2 +++ b/src/Pure/Isar/token.scala	Sat Jan 09 13:31:31 2016 +0100
     9.3 @@ -61,7 +61,7 @@
     9.4      private def other_token(keywords: Keyword.Keywords): Parser[Token] =
     9.5      {
     9.6        val letdigs1 = many1(Symbol.is_letdig)
     9.7 -      val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
     9.8 +      val sub = one(s => s == Symbol.sub_decoded || s == Symbol.sub)
     9.9        val id =
    9.10          one(Symbol.is_letter) ~
    9.11            (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
    10.1 --- a/src/Pure/Thy/html.scala	Fri Jan 08 17:41:04 2016 +0100
    10.2 +++ b/src/Pure/Thy/html.scala	Sat Jan 09 13:31:31 2016 +0100
    10.3 @@ -11,9 +11,13 @@
    10.4  {
    10.5    /* encode text with control symbols */
    10.6  
    10.7 -  val control_decoded =
    10.8 -    Map(Symbol.sub_decoded -> "sub",
    10.9 +  val control =
   10.10 +    Map(
   10.11 +      Symbol.sub -> "sub",
   10.12 +      Symbol.sub_decoded -> "sub",
   10.13 +      Symbol.sup -> "sup",
   10.14        Symbol.sup_decoded -> "sup",
   10.15 +      Symbol.bold -> "b",
   10.16        Symbol.bold_decoded -> "b")
   10.17  
   10.18    def encode(text: String): String =
   10.19 @@ -32,23 +36,23 @@
   10.20        }
   10.21      def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
   10.22  
   10.23 -    var control = ""
   10.24 +    var ctrl = ""
   10.25      for (sym <- Symbol.iterator(text)) {
   10.26 -      if (control_decoded.isDefinedAt(sym)) control = sym
   10.27 +      if (control.isDefinedAt(sym)) ctrl = sym
   10.28        else {
   10.29 -        control_decoded.get(control) match {
   10.30 +        control.get(ctrl) match {
   10.31            case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
   10.32              result ++= ("<" + elem + ">")
   10.33              encode_chars(sym)
   10.34              result ++= ("</" + elem + ">")
   10.35            case _ =>
   10.36 -            encode_chars(control)
   10.37 +            encode_chars(ctrl)
   10.38              encode_chars(sym)
   10.39          }
   10.40 -        control = ""
   10.41 +        ctrl = ""
   10.42        }
   10.43      }
   10.44 -    encode_chars(control)
   10.45 +    encode_chars(ctrl)
   10.46  
   10.47      result.toString
   10.48    }
    11.1 --- a/src/Pure/pure_thy.ML	Fri Jan 08 17:41:04 2016 +0100
    11.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 09 13:31:31 2016 +0100
    11.3 @@ -151,7 +151,7 @@
    11.4      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    11.5      ("_indexdefault", typ "index",                     Delimfix ""),
    11.6      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
    11.7 -    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
    11.8 +    ("_struct",     typ "index => logic",              NoSyn),
    11.9      ("_update_name", typ "idt",                        NoSyn),
   11.10      ("_constrainAbs", typ "'a",                        NoSyn),
   11.11      ("_position_sort", typ "tid => tid_position",      Delimfix "_"),
    12.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Jan 08 17:41:04 2016 +0100
    12.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Jan 09 13:31:31 2016 +0100
    12.3 @@ -303,16 +303,16 @@
    12.4    /* control styles */
    12.5  
    12.6    def control_sub(text_area: JEditTextArea)
    12.7 -  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    12.8 +  { Token_Markup.edit_control_style(text_area, Symbol.sub) }
    12.9  
   12.10    def control_sup(text_area: JEditTextArea)
   12.11 -  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   12.12 +  { Token_Markup.edit_control_style(text_area, Symbol.sup) }
   12.13  
   12.14    def control_bold(text_area: JEditTextArea)
   12.15 -  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   12.16 +  { Token_Markup.edit_control_style(text_area, Symbol.bold) }
   12.17  
   12.18    def control_emph(text_area: JEditTextArea)
   12.19 -  { Token_Markup.edit_control_style(text_area, Symbol.emph_decoded) }
   12.20 +  { Token_Markup.edit_control_style(text_area, Symbol.emph) }
   12.21  
   12.22    def control_reset(text_area: JEditTextArea)
   12.23    { Token_Markup.edit_control_style(text_area, "") }
    13.1 --- a/src/Tools/jEdit/src/isabelle_encoding.scala	Fri Jan 08 17:41:04 2016 +0100
    13.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Sat Jan 09 13:31:31 2016 +0100
    13.3 @@ -25,6 +25,9 @@
    13.4  
    13.5    def is_active(buffer: JEditBuffer): Boolean =
    13.6      buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
    13.7 +
    13.8 +  def maybe_decode(buffer: JEditBuffer, s: String): String =
    13.9 +    if (is_active(buffer)) Symbol.decode(s) else s
   13.10  }
   13.11  
   13.12  class Isabelle_Encoding extends Encoding
    14.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 08 17:41:04 2016 +0100
    14.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Jan 09 13:31:31 2016 +0100
    14.3 @@ -17,9 +17,8 @@
    14.4  
    14.5  class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
    14.6  {
    14.7 -  private class Symbol_Component(val symbol: String, control: Boolean) extends Button
    14.8 +  private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
    14.9    {
   14.10 -    private val decoded = Symbol.decode(symbol)
   14.11      private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
   14.12  
   14.13      font =
   14.14 @@ -28,11 +27,12 @@
   14.15          case Some(font_family) => GUI.font(family = font_family, size = font_size)
   14.16        }
   14.17      action =
   14.18 -      Action(decoded) {
   14.19 +      Action(Symbol.decode(symbol)) {
   14.20          val text_area = view.getTextArea
   14.21 -        if (control && HTML.control_decoded.isDefinedAt(decoded))
   14.22 -          Token_Markup.edit_control_style(text_area, decoded)
   14.23 -        else text_area.setSelectedText(decoded)
   14.24 +        if (is_control && HTML.control.isDefinedAt(symbol))
   14.25 +          Token_Markup.edit_control_style(text_area, symbol)
   14.26 +        else
   14.27 +          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
   14.28          text_area.requestFocus
   14.29        }
   14.30      tooltip =
    15.1 --- a/src/Tools/jEdit/src/token_markup.scala	Fri Jan 08 17:41:04 2016 +0100
    15.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jan 09 13:31:31 2016 +0100
    15.3 @@ -27,26 +27,28 @@
    15.4  {
    15.5    /* editing support for control symbols */
    15.6  
    15.7 -  def update_control_style(control: String, text: String): String =
    15.8 -  {
    15.9 -    val result = new StringBuilder
   15.10 -    for (sym <- Symbol.iterator(text) if !HTML.control_decoded.isDefinedAt(sym)) {
   15.11 -      if (Symbol.is_controllable(sym)) result ++= control
   15.12 -      result ++= sym
   15.13 -    }
   15.14 -    result.toString
   15.15 -  }
   15.16 -
   15.17    def edit_control_style(text_area: TextArea, control: String)
   15.18    {
   15.19      GUI_Thread.assert {}
   15.20  
   15.21      val buffer = text_area.getBuffer
   15.22  
   15.23 +    val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
   15.24 +
   15.25 +    def update_style(text: String): String =
   15.26 +    {
   15.27 +      val result = new StringBuilder
   15.28 +      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
   15.29 +        if (Symbol.is_controllable(sym)) result ++= control_decoded
   15.30 +        result ++= sym
   15.31 +      }
   15.32 +      result.toString
   15.33 +    }
   15.34 +
   15.35      text_area.getSelection.foreach(sel => {
   15.36        val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
   15.37        JEdit_Lib.try_get_text(buffer, before) match {
   15.38 -        case Some(s) if HTML.control_decoded.isDefinedAt(s) =>
   15.39 +        case Some(s) if HTML.control.isDefinedAt(s) =>
   15.40            text_area.extendSelection(before.start, before.stop)
   15.41          case _ =>
   15.42        }
   15.43 @@ -54,12 +56,11 @@
   15.44  
   15.45      text_area.getSelection.toList match {
   15.46        case Nil =>
   15.47 -        text_area.setSelectedText(control)
   15.48 +        text_area.setSelectedText(control_decoded)
   15.49        case sels =>
   15.50          JEdit_Lib.buffer_edit(buffer) {
   15.51            sels.foreach(sel =>
   15.52 -            text_area.setSelectedText(sel,
   15.53 -              update_control_style(control, text_area.getSelectedText(sel))))
   15.54 +            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
   15.55          }
   15.56      }
   15.57    }