
diff -r 22dcf2fc0aa2 -r 8fcf19f2168b doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 02 22:50:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 02 22:50:29 2008 +0200
@@ -24,733 +24,7 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Specification commands%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Derived specifications%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcll}
-    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
-    \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isarkeep{local{\dsh}theory} \\
-    \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isaratt \\
-    \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isarkeep{local{\dsh}theory} \\
-    \indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
-    \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
-    \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isarkeep{local{\dsh}theory} \\
-  \end{matharray}
-
-  These specification mechanisms provide a slightly more abstract view
-  than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see
-  \secref{sec:axms-thms}).  In particular, type-inference is commonly
-  available, and result names need not be given.
-
-  \begin{rail}
-    'axiomatization' target? fixes? ('where' specs)?
-    ;
-    'definition' target? (decl 'where')? thmdecl? prop
-    ;
-    'abbreviation' target? mode? (decl 'where')? prop
-    ;
-    ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
-    ;
-
-    fixes: ((name ('::' type)? mixfix? | vars) + 'and')
-    ;
-    specs: (thmdecl? props + 'and')
-    ;
-    decl: name ('::' type)? mixfix?
-    ;
-  \end{rail}
-
-  \begin{descr}
-  
-  \item [\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}] introduces several constants
-  simultaneously and states axiomatic properties for these.  The
-  constants are marked as being specified once and for all, which
-  prevents additional specifications being issued later on.
-  
-  Note that axiomatic specifications are only appropriate when
-  declaring a new logical system.  Normal applications should only use
-  definitional mechanisms!
-
-  \item [\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] produces an
-  internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification
-  given as \isa{eq}, which is then turned into a proven fact.  The
-  given proposition may deviate from internal meta-level equality
-  according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the
-  object-logic.  This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}.  End-users normally need not
-  change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup.
-  
-  Definitions may be presented with explicit arguments on the LHS, as
-  well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of
-  \isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an
-  unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}.
-  
-  \item [\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}}] introduces
-  a syntactic constant which is associated with a certain term
-  according to the meta-level equality \isa{eq}.
-  
-  Abbreviations participate in the usual type-inference process, but
-  are expanded before the logic ever sees them.  Pretty printing of
-  terms involves higher-order rewriting with rules stemming from
-  reverted abbreviations.  This needs some care to avoid overlapping
-  or looping syntactic replacements!
-  
-  The optional \isa{mode} specification restricts output to a
-  particular print mode; using ``\isa{input}'' here achieves the
-  effect of one-way abbreviations.  The mode may also include an
-  ``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax
-  declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in
-  \secref{sec:syn-trans}.
-  
-  \item [\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}] prints all constant abbreviations
-  of the current context.
-  
-  \item [\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] associates mixfix
-  syntax with an existing constant or fixed variable.  This is a
-  robust interface to the underlying \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} primitive
-  (\secref{sec:syn-trans}).  Type declaration and internal syntactic
-  representation of the given entity is retrieved from the context.
-  
-  \item [\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}] is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but removes the specified syntax annotation from the
-  present context.
-
-  \end{descr}
-
-  All of these specifications support local theory targets (cf.\
-  \secref{sec:target}).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Generic declarations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Arbitrary operations on the background context may be wrapped-up as
-  generic declaration elements.  Since the underlying concept of local
-  theories may be subject to later re-interpretation, there is an
-  additional dependency on a morphism that tells the difference of the
-  original declaration context wrt.\ the application context
-  encountered later on.  A fact declaration is an important special
-  case: it consists of a theorem which is applied to the context by
-  means of an attribute.
-
-  \begin{matharray}{rcl}
-    \indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isarkeep{local{\dsh}theory} \\
-    \indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isarkeep{local{\dsh}theory} \\
-  \end{matharray}
-
-  \begin{rail}
-    'declaration' target? text
-    ;
-    'declare' target? (thmrefs + 'and')
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d}] adds the declaration
-  function \isa{d} of ML type \verb|declaration|, to the current
-  local theory under construction.  In later application contexts, the
-  function is transformed according to the morphisms being involved in
-  the interpretation hierarchy.
-
-  \item [\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms}] declares theorems to the
-  current local theory context.  No theorem binding is involved here,
-  unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\
-  \secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect
-  of applying attributes as included in the theorem specification.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Local theory targets \label{sec:target}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A local theory target is a context managed separately within the
-  enclosing theory.  Contexts may introduce parameters (fixed
-  variables) and assumptions (hypotheses).  Definitions and theorems
-  depending on the context may be added incrementally later on.  Named
-  contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
-  (cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the
-  global theory context.
-
-  \begin{matharray}{rcll}
-    \indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{local{\dsh}theory}{theory} \\
-  \end{matharray}
-
-  \indexouternonterm{target}
-  \begin{rail}
-    'context' name 'begin'
-    ;
-
-    target: '(' 'in' name ')'
-    ;
-  \end{rail}
-
-  \begin{descr}
-  
-  \item [\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}}] recommences an
-  existing locale or class context \isa{c}.  Note that locale and
-  class definitions allow to include the \indexref{}{keyword}{begin}\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}
-  keyword as well, in order to continue the local theory immediately
-  after the initial specification.
-  
-  \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current local theory and
-  continues the enclosing global theory.  Note that a non-local
-  \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory
-  itself (\secref{sec:begin-thy}).
-  
-  \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}}] given after any local theory command
-  specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''.  This works both in a local or
-  global theory context; the current target context will be suspended
-  for this command only.  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will
-  always produce a global result independently of the current target
-  context.
-
-  \end{descr}
-
-  The exact meaning of results produced within a local theory context
-  depends on the underlying target infrastructure (locale, type class
-  etc.).  The general idea is as follows, considering a context named
-  \isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}.
-  
-  Definitions are exported by introducing a global version with
-  additional arguments; a syntactic abbreviation links the long form
-  with the abstract version of the target context.  For example,
-  \isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory
-  level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local
-  abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the
-  fixed parameter \isa{x}).
-
-  Theorems are exported by discharging the assumptions and
-  generalizing the parameters of the context.  For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary
-  \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Locales \label{sec:locale}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locales are named local contexts, consisting of a list of
-  declaration elements that are modeled after the Isar proof context
-  commands (cf.\ \secref{sec:proof-context}).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Locale specifications%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
-    \indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
-    \indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isarmeth \\
-    \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isarmeth \\
-  \end{matharray}
-
-  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
-  \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
-  \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
-  \begin{rail}
-    'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
-    ;
-    'print\_locale' '!'? localeexpr
-    ;
-    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
-    ;
-
-    contextexpr: nameref | '(' contextexpr ')' |
-    (contextexpr (name mixfix? +)) | (contextexpr + '+')
-    ;
-    contextelem: fixes | constrains | assumes | defines | notes
-    ;
-    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
-    ;
-    constrains: 'constrains' (name '::' type + 'and')
-    ;
-    assumes: 'assumes' (thmdecl? props + 'and')
-    ;
-    defines: 'defines' (thmdecl? prop proppat? + 'and')
-    ;
-    notes: 'notes' (thmdef? thmrefs + 'and')
-    ;
-    includes: 'includes' contextexpr
-    ;
-  \end{rail}
-
-  \begin{descr}
-  
-  \item [\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}}] defines a
-  new locale \isa{loc} as a context consisting of a certain view of
-  existing locales (\isa{import}) plus some additional elements
-  (\isa{body}).  Both \isa{import} and \isa{body} are optional;
-  the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty
-  locale, which may still be useful to collect declarations of facts
-  later on.  Type-inference on locale expressions automatically takes
-  care of the most general typing that the combined context elements
-  may acquire.
-
-  The \isa{import} consists of a structured context expression,
-  consisting of references to existing locales, renamed contexts, or
-  merged contexts.  Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
-  parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
-  position.  Renaming by default deletes concrete syntax, but new
-  syntax may by specified with a mixfix annotation.  An exeption of
-  this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
-  be changed.  Merging proceeds from left-to-right, suppressing any
-  duplicates stemming from different paths through the import
-  hierarchy.
-
-  The \isa{body} consists of basic context elements, further context
-  expressions may be included as well.
-
-  \begin{descr}
-
-  \item [\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}}] declares a local
-  parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both
-  are optional).  The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced
-  implicitly in this context.
-
-  \item [\hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}] introduces a type
-  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
-
-  \item [\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}]
-  introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
-  proof (cf.\ \secref{sec:proof-context}).
-
-  \item [\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}}] defines a previously
-  declared parameter.  This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a
-  proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}
-  takes an equational proposition instead of variable-term pair.  The
-  left-hand side of the equation may have additional arguments, e.g.\
-  ``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''.
-
-  \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
-  reconsiders facts within a local context.  Most notably, this may
-  include arbitrary declarations in any attribute specifications
-  included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
-
-  \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
-  in a statically scoped manner.  Only available in the long goal
-  format of \secref{sec:goals}.
-
-  In contrast, the initial \isa{import} specification of a locale
-  expression maintains a dynamic relation to the locales being
-  referenced (benefiting from any later fact declarations in the
-  obvious manner).
-
-  \end{descr}
-  
-  Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given
-  in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above
-  are illegal in locale definitions.  In the long goal format of
-  \secref{sec:goals}, term bindings may be included as expected,
-  though.
-  
-  \medskip By default, locale specifications are ``closed up'' by
-  turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
-  (modulo local definitions).  The predicate statement covers only the
-  newly specified assumptions, omitting the content of included locale
-  expressions.  The full cumulative view is only provided on export,
-  involving another predicate \isa{loc} that refers to the complete
-  specification text.
-  
-  In any case, the predicate arguments are those locale parameters
-  that actually occur in the respective piece of text.  Also note that
-  these predicates operate at the meta-level in theory, but the locale
-  packages attempts to internalize statements according to the
-  object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and
-  \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
-  \secref{sec:object-logic}).  Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
-  
-  The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option of a locale specification prevents both
-  the current \isa{loc{\isacharunderscore}axioms} and cumulative \isa{loc} predicate
-  constructions.  Predicates are also omitted for empty specification
-  texts.
-
-  \item [\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}}] prints the
-  specified locale expression in a flattened form.  The notable
-  special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
-  contents of the named locale, but keep in mind that type-inference
-  will normalize type variables according to the usual alphabetical
-  order.  The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
-  Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
-
-  \item [\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}] prints the names of all locales
-  of the current theory.
-
-  \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}]
-  repeatedly expand all introduction rules of locale predicates of the
-  theory.  While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
-  assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
-  \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
-  specifications entailed by the context, both from target and
-  \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
-  below).  New goals that are entailed by the current context are
-  discharged automatically.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Interpretation of locales%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Locale expressions (more precisely, \emph{context expressions}) may
-  be instantiated, and the instantiated facts added to the current
-  context.  This requires a proof of the instantiated specification
-  and is called \emph{locale interpretation}.  Interpretation is
-  possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
-
-  \begin{matharray}{rcl}
-    \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isartrans{theory}{proof(prove)} \\
-    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
-    \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : &  \isarkeep{theory~|~proof} \\
-  \end{matharray}
-
-  \indexouternonterm{interp}
-  \begin{rail}
-    'interpretation' (interp | name ('<' | subseteq) contextexpr)
-    ;
-    'interpret' interp
-    ;
-    'print\_interps' '!'? name
-    ;
-    instantiation: ('[' (inst+) ']')?
-    ;
-    interp: thmdecl? \\ (contextexpr instantiation |
-      name instantiation 'where' (thmdecl? prop + 'and'))
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
-
-  The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms
-  \isa{insts} and is positional.  All parameters must receive an
-  instantiation term --- with the exception of defined parameters.
-  These are, if omitted, derived from the defining equation and other
-  instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
-
-  The command generates proof obligations for the instantiated
-  specifications (assumes and defines elements).  Once these are
-  discharged by the user, instantiated facts are added to the theory
-  in a post-processing phase.
-
-  Additional equations, which are unfolded in facts during
-  post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
-  This is useful for interpreting concepts introduced through
-  definition specification elements.  The equations must be proved.
-  Note that if equations are present, the context expression is
-  restricted to a locale name.
-
-  The command is aware of interpretations already active in the
-  theory.  No proof obligations are generated for those, neither is
-  post-processing applied to their facts.  This avoids duplication of
-  interpreted facts, in particular.  Note that, in the case of a
-  locale with import, parts of the interpretation may already be
-  active.  The command will only generate proof obligations and
-  process facts for new parts.
-
-  The context expression may be preceded by a name and/or attributes.
-  These take effect in the post-processing of facts.  The name is used
-  to prefix fact names, for example to avoid accidental hiding of
-  other facts.  Attributes are applied after attributes of the
-  interpreted facts.
-
-  Adding facts to locales has the effect of adding interpreted facts
-  to the theory for all active interpretations also.  That is,
-  interpretations dynamically participate in any facts added to
-  locales.
-
-  \item [\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}]
-
-  This form of the command interprets \isa{expr} in the locale
-  \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
-  localized version of the theorem command, the proof is in the
-  context of \isa{name}.  After the proof obligation has been
-  dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
-  context \isa{name} is subsequently entered.  Note that, like
-  import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
-  Like facts of renamed context elements, facts obtained by
-  interpretation may be accessed by prefixing with the parameter
-  renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
-
-  Unlike interpretation in theories, instantiation is confined to the
-  renaming of parameters, which may be specified as part of the
-  context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
-
-  Only specification fragments of \isa{expr} that are not already
-  part of \isa{name} (be it imported, derived or a derived fragment
-  of the import) are considered by interpretation.  This enables
-  circular interpretations.
-
-  If interpretations of \isa{name} exist in the current theory, the
-  command adds interpretations for \isa{expr} as well, with the same
-  prefix and attributes, although only for fragments of \isa{expr}
-  that are not interpreted in the theory already.
-
-  \item [\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}]
-  interprets \isa{expr} in the proof context and is otherwise
-  similar to interpretation in theories.
-
-  \item [\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc}] prints the
-  interpretations of a particular locale \isa{loc} that are active
-  in the current context, either theory or proof context.  The
-  exclamation point argument triggers printing of \emph{witness}
-  theorems justifying interpretations.  These are normally omitted
-  from the output.
-  
-  \end{descr}
-
-  \begin{warn}
-    Since attributes are applied to interpreted theorems,
-    interpretation may modify the context of common proof tools, e.g.\
-    the Simplifier or Classical Reasoner.  Since the behavior of such
-    automated reasoning tools is \emph{not} stable under
-    interpretation morphisms, manual declarations might have to be
-    issued.
-  \end{warn}
-
-  \begin{warn}
-    An interpretation in a theory may subsume previous
-    interpretations.  This happens if the same specification fragment
-    is interpreted twice and the instantiation of the second
-    interpretation is more general than the interpretation of the
-    first.  A warning is issued, since it is likely that these could
-    have been generalized in the first place.  The locale package does
-    not attempt to remove subsumed interpretations.
-  \end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Classes \label{sec:class}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A class is a particular locale with \emph{exactly one} type variable
-  \isa{{\isasymalpha}}.  Beyond the underlying locale, a corresponding type class
-  is established which is interpreted logically as axiomatic type
-  class \cite{Wenzel:1997:TPHOL} whose logical content are the
-  assumptions of the locale.  Thus, classes provide the full
-  generality of locales combined with the commodity of type classes
-  (notably type-inference).  See \cite{isabelle-classes} for a short
-  tutorial.
-
-  \begin{matharray}{rcl}
-    \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
-    \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
-    \indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isarmeth \\
-  \end{matharray}
-
-  \begin{rail}
-    'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\
-      'begin'?
-    ;
-    'instantiation' (nameref + 'and') '::' arity 'begin'
-    ;
-    'instance'
-    ;
-    'subclass' target? nameref
-    ;
-    'print\_classes'
-    ;
-
-    superclassexpr: nameref | (nameref '+' superclassexpr)
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}}] defines
-  a new class \isa{c}, inheriting from \isa{superclasses}.  This
-  introduces a locale \isa{c} with import of all locales \isa{superclasses}.
-
-  Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global
-  theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter
-  \isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}.
-
-  Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted,
-  mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its
-  corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.  The
-  corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}.  This rule should be rarely needed directly
-  --- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of
-  class membership proofs.
-
-  \item [\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s\ {\isasymBEGIN}{\isachardoublequote}}] opens a theory target (cf.\
-  \secref{sec:target}) which allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding to sort \isa{s} at the
-  particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}.  A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
-  in the target body poses a goal stating these type arities.  The
-  target is concluded by an \indexref{}{command}{end}\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} command.
-
-  Note that a list of simultaneous type constructors may be given;
-  this corresponds nicely to mutual recursive type definitions, e.g.\
-  in Isabelle/HOL.
-
-  \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}] in an instantiation target body sets
-  up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}.  The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of
-  the type classes involved.  After finishing the proof, the
-  background theory will be augmented by the proven type arities.
-
-  \item [\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c}] in a class context for class
-  \isa{d} sets up a goal stating that class \isa{c} is logically
-  contained in class \isa{d}.  After finishing the proof, class
-  \isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
-
-  \item [\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] prints all classes in the current
-  theory.
-
-  \item [\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}] repeatedly expands all class
-  introduction rules of this theory.  Note that this method usually
-  needs not be named explicitly, as it is already included in the
-  default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}).  In particular,
-  instantiation of trivial (syntactic) classes may be performed by a
-  single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{The class target%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-%FIXME check
-
-  A named context may refer to a locale (cf.\ \secref{sec:target}).
-  If this locale is also a class \isa{c}, apart from the common
-  locale target behaviour the following happens.
-
-  \begin{itemize}
-
-  \item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the
-  local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}}
-  are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}
-  referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}.
-
-  \item Local theorem bindings are lifted as are assumptions.
-
-  \item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and
-  global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly.  Type inference
-  resolves ambiguities.  In rare cases, manual type annotations are
-  needed.
-  
-  \end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Axiomatic type classes \label{sec:axclass}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
-    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
-  \end{matharray}
-
-  Axiomatic type classes are Isabelle/Pure's primitive
-  \emph{definitional} interface to type classes.  For practical
-  applications, you should consider using classes
-  (cf.~\secref{sec:classes}) which provide high level interface.
-
-  \begin{rail}
-    'axclass' classdecl (axmdecl prop +)
-    ;
-    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
-    ;
-  \end{rail}
-
-  \begin{descr}
-  
-  \item [\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}}] defines an axiomatic type class as the intersection of
-  existing classes, with additional axioms holding.  Class axioms may
-  not contain more than one type variable.  The class axioms (with
-  implicit sort constraints added) are bound to the given names.
-  Furthermore a class introduction rule is generated (being bound as
-  \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
-  
-  The ``class axioms'' are stored as theorems according to the given
-  name specifications, adding \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} as name space prefix;
-  the same facts are also stored collectively as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
-  
-  \item [\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and
-  \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s{\isachardoublequote}}]
-  setup a goal stating a class relation or type arity.  The proof
-  would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish
-  the characteristic theorems of the type classes involved.  After
-  finishing the proof, the theory will be augmented by a type
-  signature declaration corresponding to the resulting theorem.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Arbitrary overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle/Pure's definitional schemes support certain forms of
-  overloading (see \secref{sec:consts}).  At most occassions
-  overloading will be used in a Haskell-like fashion together with
-  type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see
-  \secref{sec:class}).  Sometimes low-level overloading is desirable.
-  The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for
-  end-users.
-
-  \begin{matharray}{rcl}
-    \indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isartrans{theory}{local{\dsh}theory} \\
-  \end{matharray}
-
-  \begin{rail}
-    'overloading' \\
-    ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin'
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}]
-  opens a theory target (cf.\ \secref{sec:target}) which allows to
-  specify constants with overloaded definitions.  These are identified
-  by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type
-  instances.  The definitions themselves are established using common
-  specification tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as
-  reference to the corresponding constants.  The target is concluded
-  by \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}.
-
-  A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for
-  the corresponding definition, which is occasionally useful for
-  exotic overloading.  It is at the discretion of the user to avoid
-  malformed theory specifications!
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Configuration options%
+\isamarkupsection{Configuration options%
 }
 \isamarkuptrue%
 %
@@ -790,7 +64,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Proof tools%
+\isamarkupsection{Basic proof tools%
 }
 \isamarkuptrue%
 %
@@ -1031,11 +305,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{The Simplifier \label{sec:simplifier}%
+\isamarkupsection{The Simplifier \label{sec:simplifier}%
 }
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Simplification methods%
+\isamarkupsubsection{Simplification methods%
 }
 \isamarkuptrue%
 %
@@ -1110,7 +384,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Declaring rules%
+\isamarkupsubsection{Declaring rules%
 }
 \isamarkuptrue%
 %
@@ -1143,7 +417,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Simplification procedures%
+\isamarkupsubsection{Simplification procedures%
 }
 \isamarkuptrue%
 %
@@ -1189,7 +463,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Forward simplification%
+\isamarkupsubsection{Forward simplification%
 }
 \isamarkuptrue%
 %
@@ -1224,7 +498,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Low-level equational reasoning%
+\isamarkupsubsection{Low-level equational reasoning%
 }
 \isamarkuptrue%
 %
@@ -1290,11 +564,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{The Classical Reasoner \label{sec:classical}%
+\isamarkupsection{The Classical Reasoner \label{sec:classical}%
 }
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Basic methods%
+\isamarkupsubsection{Basic methods%
 }
 \isamarkuptrue%
 %
@@ -1339,7 +613,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Automated methods%
+\isamarkupsubsection{Automated methods%
 }
 \isamarkuptrue%
 %
@@ -1384,7 +658,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Combined automated methods \label{sec:clasimp}%
+\isamarkupsubsection{Combined automated methods \label{sec:clasimp}%
 }
 \isamarkuptrue%
 %
@@ -1430,7 +704,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Declaring rules%
+\isamarkupsubsection{Declaring rules%
 }
 \isamarkuptrue%
 %
@@ -1486,7 +760,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Classical operations%
+\isamarkupsubsection{Classical operations%
 }
 \isamarkuptrue%
 %
@@ -1504,355 +778,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Proof by cases and induction \label{sec:cases-induct}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Rule contexts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{}{command}{case}\hypertarget{command.case}{\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}} & : & \isartrans{proof(state)}{proof(state)} \\
-    \indexdef{}{command}{print\_cases}\hypertarget{command.print-cases}{\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
-    \indexdef{}{attribute}{case\_names}\hypertarget{attribute.case-names}{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}} & : & \isaratt \\
-    \indexdef{}{attribute}{case\_conclusion}\hypertarget{attribute.case-conclusion}{\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}} & : & \isaratt \\
-    \indexdef{}{attribute}{params}\hypertarget{attribute.params}{\hyperlink{attribute.params}{\mbox{\isa{params}}}} & : & \isaratt \\
-    \indexdef{}{attribute}{consumes}\hypertarget{attribute.consumes}{\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}} & : & \isaratt \\
-  \end{matharray}
-
-  The puristic way to build up Isar proof contexts is by explicit
-  language elements like \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}},
-  \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} (see \secref{sec:proof-context}).  This is adequate
-  for plain natural deduction, but easily becomes unwieldy in concrete
-  verification tasks, which typically involve big induction rules with
-  several cases.
-
-  The \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} command provides a shorthand to refer to a
-  local context symbolically: certain proof methods provide an
-  environment of named ``cases'' of the form \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}; the effect of ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' is then equivalent to ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.  Term bindings may be covered as well, notably
-  \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for the main conclusion.
-
-  By default, the ``terminology'' \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of
-  a case value is marked as hidden, i.e.\ there is no way to refer to
-  such parameters in the subsequent proof text.  After all, original
-  rule parameters stem from somewhere outside of the current proof
-  text.  By using the explicit form ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ y\isactrlsub {\isadigit{1}}\ {\isasymdots}\ y\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' instead, the proof author is able to
-  chose local names that fit nicely into the current context.
-
-  \medskip It is important to note that proper use of \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} does not provide means to peek at the current goal state,
-  which is not directly observable in Isar!  Nonetheless, goal
-  refinement commands do provide named cases \isa{{\isachardoublequote}goal\isactrlsub i{\isachardoublequote}}
-  for each subgoal \isa{{\isachardoublequote}i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of the resulting goal state.
-  Using this extra feature requires great care, because some bits of
-  the internal tactical machinery intrude the proof text.  In
-  particular, parameter names stemming from the left-over of automated
-  reasoning tools are usually quite unpredictable.
-
-  Under normal circumstances, the text of cases emerge from standard
-  elimination or induction rules, which in turn are derived from
-  previous theory specifications in a canonical way (say from
-  \hyperlink{command.inductive}{\mbox{\isa{\isacommand{inductive}}}} definitions).
-
-  \medskip Proper cases are only available if both the proof method
-  and the rules involved support this.  By using appropriate
-  attributes, case names, conclusions, and parameters may be also
-  declared by hand.  Thus variant versions of rules that have been
-  derived manually become ready to use in advanced case analysis
-  later.
-
-  \begin{rail}
-    'case' (caseref | '(' caseref ((name | underscore) +) ')')
-    ;
-    caseref: nameref attributes?
-    ;
-
-    'case\_names' (name +)
-    ;
-    'case\_conclusion' name (name *)
-    ;
-    'params' ((name *) + 'and')
-    ;
-    'consumes' nat?
-    ;
-  \end{rail}
-
-  \begin{descr}
-  
-  \item [\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}]
-  invokes a named local context \isa{{\isachardoublequote}c{\isacharcolon}\ x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isacharcomma}\ {\isasymphi}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymphi}\isactrlsub m{\isachardoublequote}}, as provided by an appropriate
-  proof method (such as \indexref{}{method}{cases}\hyperlink{method.cases}{\mbox{\isa{cases}}} and \indexref{}{method}{induct}\hyperlink{method.induct}{\mbox{\isa{induct}}}).
-  The command ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{{\isachardoublequote}{\isacharparenleft}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isacharparenright}{\isachardoublequote}}'' abbreviates ``\hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}''.
-
-  \item [\hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}}] prints all local contexts of the
-  current state, using Isar proof language notation.
-  
-  \item [\hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub k{\isachardoublequote}}]
-  declares names for the local contexts of premises of a theorem;
-  \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub k{\isachardoublequote}} refers to the \emph{suffix} of the
-  list of premises.
-  
-  \item [\hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isacharunderscore}conclusion}}}~\isa{{\isachardoublequote}c\ d\isactrlsub {\isadigit{1}}\ {\isasymdots}\ d\isactrlsub k{\isachardoublequote}}] declares names for the conclusions of a named premise
-  \isa{c}; here \isa{{\isachardoublequote}d\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlsub k{\isachardoublequote}} refers to the
-  prefix of arguments of a logical formula built by nesting a binary
-  connective (e.g.\ \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}).
-  
-  Note that proof methods such as \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} already provide a default name for the conclusion as a
-  whole.  The need to name subformulas only arises with cases that
-  split into several sub-cases, as in common co-induction rules.
-
-  \item [\hyperlink{attribute.params}{\mbox{\isa{params}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] renames the innermost parameters of
-  premises \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n{\isachardoublequote}} of some theorem.  An empty list of names
-  may be given to skip positions, leaving the present parameters
-  unchanged.
-  
-  Note that the default usage of case rules does \emph{not} directly
-  expose parameters to the proof context.
-  
-  \item [\hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{n}] declares the number of
-  ``major premises'' of a rule, i.e.\ the number of facts to be
-  consumed when it is applied by an appropriate proof method.  The
-  default value of \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} is \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}, which is
-  appropriate for the usual kind of cases and induction rules for
-  inductive sets (cf.\ \secref{sec:hol-inductive}).  Rules without any
-  \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declaration given are treated as if
-  \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} had been specified.
-  
-  Note that explicit \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}} declarations are only
-  rarely needed; this is already taken care of automatically by the
-  higher-level \hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and
-  \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}} declarations.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Proof methods%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isarmeth \\
-    \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isarmeth \\
-    \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isarmeth \\
-  \end{matharray}
-
-  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
-  methods provide a uniform interface to common proof techniques over
-  datatypes, inductive predicates (or sets), recursive functions etc.
-  The corresponding rules may be specified and instantiated in a
-  casual manner.  Furthermore, these methods provide named local
-  contexts that may be invoked via the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}} proof command
-  within the subsequent proof text.  This accommodates compact proof
-  texts even when reasoning about large specifications.
-
-  The \hyperlink{method.induct}{\mbox{\isa{induct}}} method also provides some additional
-  infrastructure in order to be applicable to structure statements
-  (either using explicit meta-level connectives, or including facts
-  and parameters separately).  This avoids cumbersome encoding of
-  ``strengthened'' inductive statements within the object-logic.
-
-  \begin{rail}
-    'cases' (insts * 'and') rule?
-    ;
-    'induct' (definsts * 'and') \\ arbitrary? taking? rule?
-    ;
-    'coinduct' insts taking rule?
-    ;
-
-    rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
-    ;
-    definst: name ('==' | equiv) term | inst
-    ;
-    definsts: ( definst *)
-    ;
-    arbitrary: 'arbitrary' ':' ((term *) 'and' +)
-    ;
-    taking: 'taking' ':' insts
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{method.cases}{\mbox{\isa{cases}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] applies method \hyperlink{method.rule}{\mbox{\isa{rule}}} with an appropriate case distinction theorem, instantiated to
-  the subjects \isa{insts}.  Symbolic case names are bound according
-  to the rule's local contexts.
-
-  The rule is determined as follows, according to the facts and
-  arguments passed to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method:
-
-  \medskip
-  \begin{tabular}{llll}
-    facts           &                 & arguments   & rule \\\hline
-                    & \hyperlink{method.cases}{\mbox{\isa{cases}}} &             & classical case split \\
-                    & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{t}   & datatype exhaustion (type of \isa{t}) \\
-    \isa{{\isachardoublequote}{\isasymturnstile}\ A\ t{\isachardoublequote}} & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & inductive predicate/set elimination (of \isa{A}) \\
-    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}     & \hyperlink{method.cases}{\mbox{\isa{cases}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
-  \end{tabular}
-  \medskip
-
-  Several instantiations may be given, referring to the \emph{suffix}
-  of premises of the case rule; within each premise, the \emph{prefix}
-  of variables is instantiated.  In most situations, only a single
-  term needs to be specified; this refers to the first variable of the
-  last premise (it is usually the same for all cases).
-
-  \item [\hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}}] is analogous to the
-  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
-  determined as follows:
-
-  \medskip
-  \begin{tabular}{llll}
-    facts           &                  & arguments            & rule \\\hline
-                    & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}P\ x{\isachardoublequote}}        & datatype induction (type of \isa{x}) \\
-    \isa{{\isachardoublequote}{\isasymturnstile}\ A\ x{\isachardoublequote}} & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}          & predicate/set induction (of \isa{A}) \\
-    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}     & \hyperlink{method.induct}{\mbox{\isa{induct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
-  \end{tabular}
-  \medskip
-  
-  Several instantiations may be given, each referring to some part of
-  a mutual inductive definition or datatype --- only related partial
-  induction rules may be used together, though.  Any of the lists of
-  terms \isa{{\isachardoublequote}P{\isacharcomma}\ x{\isacharcomma}\ {\isasymdots}{\isachardoublequote}} refers to the \emph{suffix} of variables
-  present in the induction rule.  This enables the writer to specify
-  only induction variables, or both predicates and variables, for
-  example.
-  
-  Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
-  introduce local definitions, which are inserted into the claim and
-  discharged after applying the induction rule.  Equalities reappear
-  in the inductive cases, but have been transformed according to the
-  induction principle being involved here.  In order to achieve
-  practically useful induction hypotheses, some variables occurring in
-  \isa{t} need to be fixed (see below).
-  
-  The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
-  specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction.  Thus
-  induction hypotheses may become sufficiently general to get the
-  proof through.  Together with definitional instantiations, one may
-  effectively perform induction over expressions of a certain
-  structure.
-  
-  The optional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
-  specification provides additional instantiations of a prefix of
-  pending variables in the rule.  Such schematic induction rules
-  rarely occur in practice, though.
-
-  \item [\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}~\isa{{\isachardoublequote}inst\ R{\isachardoublequote}}] is analogous to the
-  \hyperlink{method.induct}{\mbox{\isa{induct}}} method, but refers to coinduction rules, which are
-  determined as follows:
-
-  \medskip
-  \begin{tabular}{llll}
-    goal          &                    & arguments & rule \\\hline
-                  & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{x} & type coinduction (type of \isa{x}) \\
-    \isa{{\isachardoublequote}A\ x{\isachardoublequote}} & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} & predicate/set coinduction (of \isa{A}) \\
-    \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}   & \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} & \isa{{\isachardoublequote}{\isasymdots}\ rule{\isacharcolon}\ R{\isachardoublequote}} & explicit rule \isa{R} \\
-  \end{tabular}
-  
-  Coinduction is the dual of induction.  Induction essentially
-  eliminates \isa{{\isachardoublequote}A\ x{\isachardoublequote}} towards a generic result \isa{{\isachardoublequote}P\ x{\isachardoublequote}},
-  while coinduction introduces \isa{{\isachardoublequote}A\ x{\isachardoublequote}} starting with \isa{{\isachardoublequote}B\ x{\isachardoublequote}}, for a suitable ``bisimulation'' \isa{B}.  The cases of a
-  coinduct rule are typically named after the predicates or sets being
-  covered, while the conclusions consist of several alternatives being
-  named after the individual destructor patterns.
-  
-  The given instantiation refers to the \emph{suffix} of variables
-  occurring in the rule's major premise, or conclusion if unavailable.
-  An additional ``\isa{{\isachardoublequote}taking{\isacharcolon}\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}''
-  specification may be required in order to specify the bisimulation
-  to be used in the coinduction step.
-
-  \end{descr}
-
-  Above methods produce named local contexts, as determined by the
-  instantiated rule as given in the text.  Beyond that, the \hyperlink{method.induct}{\mbox{\isa{induct}}} and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} methods guess further instantiations
-  from the goal specification itself.  Any persisting unresolved
-  schematic variables of the resulting rule will render the the
-  corresponding case invalid.  The term binding \hyperlink{variable.?case}{\mbox{\isa{{\isacharquery}case}}} for
-  the conclusion will be provided with each case, provided that term
-  is fully specified.
-
-  The \hyperlink{command.print-cases}{\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}} command prints all named cases present
-  in the current proof state.
-
-  \medskip Despite the additional infrastructure, both \hyperlink{method.cases}{\mbox{\isa{cases}}}
-  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}} merely apply a certain rule, after
-  instantiation, while conforming due to the usual way of monotonic
-  natural deduction: the context of a structured statement \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ {\isasymdots}{\isachardoublequote}}
-  reappears unchanged after the case split.
-
-  The \hyperlink{method.induct}{\mbox{\isa{induct}}} method is fundamentally different in this
-  respect: the meta-level structure is passed through the
-  ``recursive'' course involved in the induction.  Thus the original
-  statement is basically replaced by separate copies, corresponding to
-  the induction hypotheses and conclusion; the original goal context
-  is no longer available.  Thus local assumptions, fixed parameters
-  and definitions effectively participate in the inductive rephrasing
-  of the original statement.
-
-  In induction proofs, local assumptions introduced by cases are split
-  into two different kinds: \isa{hyps} stemming from the rule and
-  \isa{prems} from the goal statement.  This is reflected in the
-  extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isachardot}hyps} and \isa{c{\isachardot}prems},
-  as well as fact \isa{c} to hold the all-inclusive list.
-
-  \medskip Facts presented to either method are consumed according to
-  the number of ``major premises'' of the rule involved, which is
-  usually 0 for plain cases and induction rules of datatypes etc.\ and
-  1 for rules of inductive predicates or sets and the like.  The
-  remaining facts are inserted into the goal verbatim before the
-  actual \isa{cases}, \isa{induct}, or \isa{coinduct} rule is
-  applied.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Declaring rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-    \indexdef{}{command}{print\_induct\_rules}\hypertarget{command.print-induct-rules}{\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
-    \indexdef{}{attribute}{cases}\hypertarget{attribute.cases}{\hyperlink{attribute.cases}{\mbox{\isa{cases}}}} & : & \isaratt \\
-    \indexdef{}{attribute}{induct}\hypertarget{attribute.induct}{\hyperlink{attribute.induct}{\mbox{\isa{induct}}}} & : & \isaratt \\
-    \indexdef{}{attribute}{coinduct}\hypertarget{attribute.coinduct}{\hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}} & : & \isaratt \\
-  \end{matharray}
-
-  \begin{rail}
-    'cases' spec
-    ;
-    'induct' spec
-    ;
-    'coinduct' spec
-    ;
-
-    spec: ('type' | 'pred' | 'set') ':' nameref
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
-  rules for predicates (or sets) and types of the current context.
-  
-  \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{coinduct}}}] (as attributes) augment the corresponding context of
-  rules for reasoning about (co)inductive predicates (or sets) and
-  types, using the corresponding methods of the same name.  Certain
-  definitional packages of object-logics usually declare emerging
-  cases and induction rules as expected, so users rarely need to
-  intervene.
-  
-  Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
-  cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}
-  declaration is taken care of automatically: \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{0}}} is specified for ``type'' rules and \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}~\isa{{\isadigit{1}}} for ``predicate'' / ``set'' rules.
-
-  \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{General logic setup \label{sec:object-logic}%
 }
 \isamarkuptrue%




