diff -r a16b18fd6299 -r 6a3f7941c3a0 doc-src/IsarImplementation/Thy/document/Isar.tex
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Fri Oct 22 20:51:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Fri Oct 22 20:57:33 2010 +0100
@@ -23,16 +23,33 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The primary Isar language consists of three main categories of
-  language elements:
+The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
+  consists of three main categories of language elements:
 
   \begin{enumerate}
 
-  \item Proof commands
+  \item Proof \emph{commands} define the primary language of
+  transactions of the underlying Isar/VM interpreter.  Typical
+  examples are \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}, \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}, and \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}.
+
+  Composing proof commands according to the rules of the Isar/VM leads
+  to expressions of structured proof text, such that both the machine
+  and the human reader can give it a meaning as formal reasoning.
 
-  \item Proof methods
+  \item Proof \emph{methods} define a secondary language of mixed
+  forward-backward refinement steps involving facts and goals.
+  Typical examples are \hyperlink{method.rule}{\mbox{\isa{rule}}}, \hyperlink{method.unfold}{\mbox{\isa{unfold}}}, and \hyperlink{method.simp}{\mbox{\isa{simp}}}.
 
-  \item Attributes
+  Methods can occur in certain well-defined parts of the Isar proof
+  language, say as arguments to \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}, \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}},
+  or \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}.
+
+  \item \emph{Attributes} define a tertiary language of small
+  annotations to theorems being defined or referenced.  Attributes can
+  modify both the context and the theorem.
+
+  Typical examples are \hyperlink{attribute.intro}{\mbox{\isa{intro}}} (which affects the context),
+  and \hyperlink{attribute.symmetric}{\mbox{\isa{symmetric}}} (which affects the theorem).
 
   \end{enumerate}%
 \end{isamarkuptext}%
@@ -43,7 +60,227 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+A \emph{proof command} is state transition of the Isar/VM
+  proof interpreter.
+
+  In principle, Isar proof commands could be defined in
+  user-space as well.  The system is built like that in the first
+  place: part of the commands are primitive, the other part is defined
+  as derived elements.  Adding to the genuine structured proof
+  language requires profound understanding of the Isar/VM machinery,
+  though, so this is beyond the scope of this manual.
+
+  What can be done realistically is to define some diagnostic commands
+  that inspect the general state of the Isar/VM, and report some
+  feedback to the user.  Typically this involves checking of the
+  linguistic \emph{mode} of a proof state, or peeking at the pending
+  goals (if available).
+
+  Another common application is to define a toplevel command that
+  poses a problem to the user as Isar proof state and stores the final
+  result in a suitable context data slot.  Thus a proof can be
+  incorporated into the context of some user-space tool, without
+  modifying the Isar proof language itself.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{Proof.state}\verb|type Proof.state| \\
+  \indexdef{}{ML}{Proof.assert\_forward}\verb|Proof.assert_forward: Proof.state -> Proof.state| \\
+  \indexdef{}{ML}{Proof.assert\_chain}\verb|Proof.assert_chain: Proof.state -> Proof.state| \\
+  \indexdef{}{ML}{Proof.assert\_backward}\verb|Proof.assert_backward: Proof.state -> Proof.state| \\
+  \indexdef{}{ML}{Proof.simple\_goal}\verb|Proof.simple_goal: Proof.state -> {context: Proof.context, goal: thm}| \\
+  \indexdef{}{ML}{Proof.goal}\verb|Proof.goal: Proof.state ->|\isasep\isanewline%
+\verb|  {context: Proof.context, facts: thm list, goal: thm}| \\
+  \indexdef{}{ML}{Proof.raw\_goal}\verb|Proof.raw_goal: Proof.state ->|\isasep\isanewline%
+\verb|  {context: Proof.context, facts: thm list, goal: thm}| \\
+  \indexdef{}{ML}{Proof.theorem}\verb|Proof.theorem: Method.text option ->|\isasep\isanewline%
+\verb|  (thm list list -> Proof.context -> Proof.context) ->|\isasep\isanewline%
+\verb|  (term * term list) list list -> Proof.context -> Proof.state| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type \verb|Proof.state| represents Isar proof states.
+  This is a block-structured configuration with proof context,
+  linguistic mode, and optional goal.  The latter consists of goal
+  context, goal facts (``\isa{using}''), and tactical goal state
+  (see \secref{sec:tactical-goals}).
+
+  The general idea is that the facts shall contribute to the
+  refinement of some parts of the tactical goal --- how exactly is
+  defined by the proof method that is applied in that situation.
+
+  \item \verb|Proof.assert_forward|, \verb|Proof.assert_chain|, \verb|Proof.assert_backward| are partial identity functions that fail
+  unless a certain linguistic mode is active, namely ``\isa{proof{\isacharparenleft}state{\isacharparenright}}'', ``\isa{proof{\isacharparenleft}chain{\isacharparenright}}'', ``\isa{proof{\isacharparenleft}prove{\isacharparenright}}'', respectively (using the terminology of
+  \cite{isabelle-isar-ref}).
+
+  It is advisable study the implementations of existing proof commands
+  for suitable modes to be asserted.
+
+  \item \verb|Proof.simple_goal|~\isa{state} returns the structured
+  Isar goal (if available) in the form seen by ``simple'' methods
+  (like \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.blast}{\mbox{\isa{blast}}}).  The Isar goal facts are
+  already inserted as premises into the subgoals, which are presented
+  individually as in \verb|Proof.goal|.
+
+  \item \verb|Proof.goal|~\isa{state} returns the structured Isar
+  goal (if available) in the form seen by regular methods (like
+  \hyperlink{method.rule}{\mbox{\isa{rule}}}).  The auxiliary internal encoding of Pure
+  conjunctions is split into individual subgoals as usual.
+
+  \item \verb|Proof.raw_goal|~\isa{state} returns the structured
+  Isar goal (if available) in the raw internal form seen by ``raw''
+  methods (like \hyperlink{method.induct}{\mbox{\isa{induct}}}).  This form is rarely appropriate
+  for dignostic tools; \verb|Proof.simple_goal| or \verb|Proof.goal|
+  should be used in most situations.
+
+  \item \verb|Proof.theorem|~\isa{before{\isacharunderscore}qed\ after{\isacharunderscore}qed\ statement\ ctxt}
+  initializes a toplevel Isar proof state within a given context.
+
+  The optional \isa{before{\isacharunderscore}qed} method is applied at the end of
+  the proof, just before extracting the result (this feature is rarely
+  used).
+
+  The \isa{after{\isacharunderscore}qed} continuation receives the extracted result
+  in order to apply it to the final context in a suitable way (e.g.\
+  storing named facts).  Note that at this generic level the target
+  context is specified as \verb|Proof.context|, but the usual
+  wrapping of toplevel proofs into command transactions will provide a
+  \verb|local_theory| here (see also \chref{ch:local-theory}).
+  This usually affects the way how results are stored.
+
+  The \isa{statement} is given as a nested list of terms, each
+  associated with optional \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns as usual in the
+  Isar source language.  The original list structure over terms is
+  turned into one over theorems when \isa{after{\isacharunderscore}qed} is invoked.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+  \indexdef{}{ML antiquotation}{Isar.goal}\hypertarget{ML antiquotation.Isar.goal}{\hyperlink{ML antiquotation.Isar.goal}{\mbox{\isa{Isar{\isachardot}goal}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item \isa{{\isacharat}{\isacharbraceleft}Isar{\isachardot}goal{\isacharbraceright}} refers to the regular goal state (if
+  available) of the current proof state managed by the Isar toplevel
+  --- as abstract value.
+
+  This only works for diagnostic ML commands, such as \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example peeks at a certain goal configuration.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{have}\isamarkupfalse%
+\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ \ \ \ \ val\ n\ {\isacharequal}\ Thm{\isachardot}nprems{\isacharunderscore}of\ {\isacharparenleft}{\isacharhash}goal\ %
+\isaantiq
+Isar{\isachardot}goal%
+\endisaantiq
+{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{3}}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ \ \ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Here we see 3 individual subgoals in the same way as regular
+  proof methods would do.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -52,19 +289,627 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+A \isa{method} is a function \isa{context\ {\isasymrightarrow}\ thm\isactrlsup {\isacharasterisk}\ {\isasymrightarrow}\ goal\ {\isasymrightarrow}\ {\isacharparenleft}cases\ {\isasymtimes}\ goal{\isacharparenright}\isactrlsup {\isacharasterisk}\isactrlsup {\isacharasterisk}} that operates on the full Isar goal
+  configuration with context, goal facts, and tactical goal state and
+  enumerates possible follow-up goal states, with the potential
+  addition of named extensions of the proof context (\emph{cases}).
+  The latter feature is rarely used.
+
+  This means a proof method is like a structurally enhanced tactic
+  (cf.\ \secref{sec:tactics}).  The well-formedness conditions for
+  tactics need to hold for methods accordingly, with the following
+  additions.
+
+  \begin{itemize}
+
+  \item Goal addressing is further limited either to operate either
+  uniformly on \emph{all} subgoals, or specifically on the
+  \emph{first} subgoal.
+
+  Exception: old-style tactic emulations that are embedded into the
+  method space, e.g.\ \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}.
+
+  \item A non-trivial method always needs to make progress: an
+  identical follow-up goal state has to be avoided.\footnote{This
+  enables the user to write method expressions like \isa{meth\isactrlsup {\isacharplus}}
+  without looping, while the trivial do-nothing case can be recovered
+  via \isa{meth\isactrlsup {\isacharquery}}.}
+
+  Exception: trivial stuttering steps, such as ``\hyperlink{method.-}{\mbox{\isa{{\isacharminus}}}}'' or
+  \hyperlink{method.succeed}{\mbox{\isa{succeed}}}.
+
+  \item Goal facts passed to the method must not be ignored.  If there
+  is no sensible use of facts outside the goal state, facts should be
+  inserted into the subgoals that are addressed by the method.
+
+  \end{itemize}
+
+  \medskip Syntactically, the language of proof methods is embedded
+  into Isar as arguments to certain commands, e.g.\ \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} or
+  \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}.  User-space additions are reasonably easy by
+  plugging suitable method-valued parser functions into the framework,
+  using the \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} command, for example.
+
+  To get a better idea about the range of possibilities, consider the
+  following Isar proof schemes.  First some general form of structured
+  proof text:
+
+  \medskip
+  \begin{tabular}{l}
+  \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{facts\isactrlsub {\isadigit{1}}}~\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{props}~\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isactrlsub {\isadigit{2}}} \\
+  \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isacharparenleft}initial{\isacharunderscore}method{\isacharparenright}} \\
+  \quad\isa{body} \\
+  \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isacharparenleft}terminal{\isacharunderscore}method{\isacharparenright}} \\
+  \end{tabular}
+  \medskip
+
+  The goal configuration consists of \isa{facts\isactrlsub {\isadigit{1}}} and \isa{facts\isactrlsub {\isadigit{2}}} appended in that order, and various \isa{props} being
+  claimed here.  The \isa{initial{\isacharunderscore}method} is invoked with facts
+  and goals together and refines the problem to something that is
+  handled recursively in the proof \isa{body}.  The \isa{terminal{\isacharunderscore}method} has another chance to finish-off any remaining
+  subgoals, but it does not see the facts of the initial step.
+
+  \medskip The second pattern illustrates unstructured proof scripts:
+
+  \medskip
+  \begin{tabular}{l}
+  \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{props} \\
+  \quad\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isactrlsub {\isadigit{1}}}~\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isactrlsub {\isadigit{1}}} \\
+  \quad\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isactrlsub {\isadigit{2}}} \\
+  \quad\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{facts\isactrlsub {\isadigit{3}}}~\hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}}~\isa{method\isactrlsub {\isadigit{3}}} \\
+  \quad\hyperlink{command.done}{\mbox{\isa{\isacommand{done}}}} \\
+  \end{tabular}
+  \medskip
+
+  The \isa{method\isactrlsub {\isadigit{1}}} operates on the original claim together while
+  using \isa{facts\isactrlsub {\isadigit{1}}}.  Since the \hyperlink{command.apply}{\mbox{\isa{\isacommand{apply}}}} command
+  structurally resets the facts, the \isa{method\isactrlsub {\isadigit{2}}} will operate on
+  the remaining goal state without facts.  The \isa{method\isactrlsub {\isadigit{3}}} will
+  see again a collection of \isa{facts\isactrlsub {\isadigit{3}}} that has been inserted
+  into the script explicitly.
+
+  \medskip Empirically, Isar proof methods can be categorized as
+  follows.
+
+  \begin{enumerate}
+
+  \item \emph{Special method with cases} with named context additions
+  associated with the follow-up goal state.
+
+  Example: \hyperlink{method.induct}{\mbox{\isa{induct}}}, which is also a ``raw'' method since it
+  operates on the internal representation of simultaneous claims as
+  Pure conjunction, instead of separate subgoals.
+
+  \item \emph{Structured method} with strong emphasis on facts outside
+  the goal state.
+
+  Example: \hyperlink{method.rule}{\mbox{\isa{rule}}}, which captures the key ideas behind
+  structured reasoning in Isar in purest form.
+
+  \item \emph{Simple method} with weaker emphasis on facts, which are
+  inserted into subgoals to emulate old-style tactical as
+  ``premises''.
+
+  Examples: \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}}.
+
+  \item \emph{Old-style tactic emulation} with detailed numeric goal
+  addressing and explicit references to entities of the internal goal
+  state (which are otherwise invisible from proper Isar proof text).
+  To make the special non-standard status clear, the naming convention
+  \isa{foo{\isacharunderscore}tac} needs to be observed.
+
+  Example: \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}}.
+
+  \end{enumerate}
+
+  When implementing proof methods, it is advisable to study existing
+  implementations carefully and imitate the typical ``boiler plate''
+  for context-sensitive parsing and further combinators to wrap-up
+  tactic expressions as methods.\footnote{Aliases or abbreviations of
+  the standard method combinators should be avoided.  Note that from
+  Isabelle99 until Isabelle2009 the system did provide various odd
+  combinations of method wrappers that made user applications more
+  complicated than necessary.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{Proof.method}\verb|type Proof.method| \\
+  \indexdef{}{ML}{METHOD\_CASES}\verb|METHOD_CASES: (thm list -> cases_tactic) -> Proof.method| \\
+  \indexdef{}{ML}{METHOD}\verb|METHOD: (thm list -> tactic) -> Proof.method| \\
+  \indexdef{}{ML}{SIMPLE\_METHOD}\verb|SIMPLE_METHOD: tactic -> Proof.method| \\
+  \indexdef{}{ML}{SIMPLE\_METHOD'}\verb|SIMPLE_METHOD': (int -> tactic) -> Proof.method| \\
+  \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
+  \indexdef{}{ML}{Method.insert\_tac}\verb|Method.insert_tac: thm list -> int -> tactic| \\
+  \indexdef{}{ML}{Method.setup}\verb|Method.setup: binding -> (Proof.context -> Proof.method) context_parser ->|\isasep\isanewline%
+\verb|  string -> theory -> theory| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type \verb|Proof.method| represents proof methods as
+  abstract type.
+
+  \item \verb|METHOD_CASES|~\isa{{\isacharparenleft}fn\ facts\ {\isacharequal}{\isachargreater}\ cases{\isacharunderscore}tactic{\isacharparenright}} wraps
+  \isa{cases{\isacharunderscore}tactic} depending on goal facts as proof method with
+  cases; the goal context is passed via method syntax.
+
+  \item \verb|METHOD|~\isa{{\isacharparenleft}fn\ facts\ {\isacharequal}{\isachargreater}\ tactic{\isacharparenright}} wraps \isa{tactic} depending on goal facts as regular proof method; the goal
+  context is passed via method syntax.
+
+  \item \verb|SIMPLE_METHOD|~\isa{tactic} wraps a tactic that
+  addresses all subgoals uniformly as simple proof method.  Goal facts
+  are already inserted into all subgoals before \isa{tactic} is
+  applied.
+
+  \item \verb|SIMPLE_METHOD'|~\isa{tactic} wraps a tactic that
+  addresses a specific subgoal as simple proof method.  Goal facts are
+  already inserted into the first subgoal before \isa{tactic} is
+  applied to the same.
+
+  \item \verb|HEADGOAL|~\isa{tactic} applies \isa{tactic} to
+  the first subgoal.  This is convenient to reproduce part the \verb|SIMPLE_METHOD'| wrapping within regular \verb|METHOD|, for example.
+
+  \item \verb|Method.insert_tac|~\isa{facts\ i} inserts \isa{facts} into subgoal \isa{i}.  This is convenient to reproduce
+  part of the \verb|SIMPLE_METHOD| or \verb|SIMPLE_METHOD'| wrapping
+  within regular \verb|METHOD|, for example.
+
+  \item \verb|Method.setup|~\isa{name\ parser\ description} provides
+  the functionality of the Isar command \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} as ML
+  function.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+See also \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} in
+  \cite{isabelle-isar-ref} which includes some abstract examples.
+
+  \medskip The following toy examples illustrate how the goal facts
+  and state are passed to proof methods.  The pre-defined proof method
+  called ``\hyperlink{method.tactic}{\mbox{\isa{tactic}}}'' wraps ML source of type \verb|tactic| (abstracted over \verb|facts|).  This allows immediate
+  experimentation without parsing of concrete syntax.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Attributes%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{assume}\isamarkupfalse%
+\ a{\isacharcolon}\ A\ \isakeyword{and}\ b{\isacharcolon}\ B\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ rtac\ %
+\isaantiq
+thm\ conjI%
+\endisaantiq
+\ {\isadigit{1}}\ {\isacharverbatimclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{using}\isamarkupfalse%
+\ a\ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ resolve{\isacharunderscore}tac\ facts\ {\isadigit{1}}\ {\isacharverbatimclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{using}\isamarkupfalse%
+\ b\ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ resolve{\isacharunderscore}tac\ facts\ {\isadigit{1}}\ {\isacharverbatimclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{using}\isamarkupfalse%
+\ a\ \isakeyword{and}\ b%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ \ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharat}{\isacharbraceleft}Isar{\isachardot}goal{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+\ \ \ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ Method{\isachardot}insert{\isacharunderscore}tac\ facts\ {\isadigit{1}}\ {\isacharverbatimclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}tactic\ {\isacharverbatimopen}\ {\isacharparenleft}rtac\ %
+\isaantiq
+thm\ conjI%
+\endisaantiq
+\ THEN{\isacharunderscore}ALL{\isacharunderscore}NEW\ atac{\isacharparenright}\ {\isadigit{1}}\ {\isacharverbatimclose}{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\medskip The next example implements a method that simplifies
+  the first subgoal by rewrite rules given as arguments.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}simp\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms\ {\isacharequal}{\isachargreater}\ fn\ ctxt\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ CHANGED\ {\isacharparenleft}asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}HOL{\isacharunderscore}basic{\isacharunderscore}ss\ addsimps\ thms{\isacharparenright}\ i{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+{\isacharverbatimclose}\ {\isachardoublequoteopen}rewrite\ subgoal\ by\ given\ rules{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The concrete syntax wrapping of \hyperlink{command.method-setup}{\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}}} always
+  passes-through the proof context at the end of parsing, but it is
+  not used in this example.
+
+  The \verb|Attrib.thms| parser produces a list of theorems from the
+  usual Isar syntax involving attribute expressions etc.\ (syntax
+  category \hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}).  The resulting \verb|thms| are
+  added to \verb|HOL_basic_ss| which already contains the basic
+  Simplifier setup for HOL.
+
+  The tactic \verb|asm_full_simp_tac| is the one that is also used in
+  method \hyperlink{method.simp}{\mbox{\isa{simp}}} by default.  The extra wrapping by the \verb|CHANGED| tactical ensures progress of simplification: identical goal
+  states are filtered out explicitly to make the raw tactic conform to
+  standard Isar method behaviour.
+
+  \medskip Method \hyperlink{method.my-simp}{\mbox{\isa{my{\isacharunderscore}simp}}} can be used in Isar proofs like
+  this:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ a\ b\ c\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ a{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ b{\isacharcolon}\ {\isachardoublequoteopen}b\ {\isacharequal}\ c{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}a\ {\isacharequal}\ c{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}my{\isacharunderscore}simp\ a\ b{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Here is a similar method that operates on all subgoals,
+  instead of just the first one.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}simp{\isacharunderscore}all\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms\ {\isacharequal}{\isachargreater}\ fn\ ctxt\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ SIMPLE{\isacharunderscore}METHOD\isanewline
+\ \ \ \ \ \ {\isacharparenleft}CHANGED\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}ALLGOALS\ {\isacharparenleft}asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\isanewline
+\ \ \ \ \ \ \ \ \ \ {\isacharparenleft}HOL{\isacharunderscore}basic{\isacharunderscore}ss\ addsimps\ thms{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+{\isacharverbatimclose}\ {\isachardoublequoteopen}rewrite\ all\ subgoals\ by\ given\ rules{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ a\ b\ c\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ a{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ b{\isacharcolon}\ {\isachardoublequoteopen}b\ {\isacharequal}\ c{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}a\ {\isacharequal}\ c{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}c\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}my{\isacharunderscore}simp{\isacharunderscore}all\ a\ b{\isacharparenright}\isanewline
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\medskip Apart from explicit arguments, common proof methods
+  typically work with a default configuration provided by the context.
+  As a shortcut to rule management we use a cheap solution via functor
+  \verb|Named_Thms| (see also \hyperlink{file.~~/src/Pure/Tools/named-thms.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}named{\isacharunderscore}thms{\isachardot}ML}}}}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ structure\ My{\isacharunderscore}Simps\ {\isacharequal}\isanewline
+\ \ \ \ Named{\isacharunderscore}Thms\isanewline
+\ \ \ \ \ \ {\isacharparenleft}val\ name\ {\isacharequal}\ {\isachardoublequote}my{\isacharunderscore}simp{\isachardoublequote}\ val\ description\ {\isacharequal}\ {\isachardoublequote}my{\isacharunderscore}simp\ rule{\isachardoublequote}{\isacharparenright}\isanewline
+{\isacharverbatimclose}\isanewline
+\isacommand{setup}\isamarkupfalse%
+\ My{\isacharunderscore}Simps{\isachardot}setup%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+This provides ML access to a list of theorems in canonical
+  declaration order via \verb|My_Simps.get|.  The user can add or
+  delete rules via the attribute \hyperlink{attribute.my-simp}{\mbox{\isa{my{\isacharunderscore}simp}}}.  The actual
+  proof method is now defined as before, but we append the explicit
+  arguments and the rules from the context.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{method{\isacharunderscore}setup}\isamarkupfalse%
+\ my{\isacharunderscore}simp{\isacharprime}\ {\isacharequal}\ {\isacharverbatimopen}\isanewline
+\ \ Attrib{\isachardot}thms\ {\isachargreater}{\isachargreater}\ {\isacharparenleft}fn\ thms\ {\isacharequal}{\isachargreater}\ fn\ ctxt\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ SIMPLE{\isacharunderscore}METHOD{\isacharprime}\ {\isacharparenleft}fn\ i\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ CHANGED\ {\isacharparenleft}asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}HOL{\isacharunderscore}basic{\isacharunderscore}ss\ addsimps\ {\isacharparenleft}thms\ {\isacharat}\ My{\isacharunderscore}Simps{\isachardot}get\ ctxt{\isacharparenright}{\isacharparenright}\ i{\isacharparenright}{\isacharparenright}{\isacharparenright}\isanewline
+{\isacharverbatimclose}\ {\isachardoublequoteopen}rewrite\ subgoal\ by\ given\ rules\ and\ my{\isacharunderscore}simp\ rules\ from\ the\ context{\isachardoublequoteclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\medskip Method \hyperlink{method.my-simp'}{\mbox{\isa{my{\isacharunderscore}simp{\isacharprime}}}} can be used in Isar proofs
+  like this:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ a\ b\ c\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isacharbrackleft}my{\isacharunderscore}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}a\ {\isasymequiv}\ b{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isacharbrackleft}my{\isacharunderscore}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}b\ {\isasymequiv}\ c{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}a\ {\isasymequiv}\ c{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ my{\isacharunderscore}simp{\isacharprime}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\medskip The \hyperlink{method.my-simp}{\mbox{\isa{my{\isacharunderscore}simp}}} variants defined above are
+  ``simple'' methods, i.e.\ the goal facts are merely inserted as goal
+  premises by the \verb|SIMPLE_METHOD'| or \verb|SIMPLE_METHOD| wrapper.
+  For proof methods that are similar to the standard collection of
+  \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\isa{blast}}}, \hyperlink{method.auto}{\mbox{\isa{auto}}} little more can be
+  done here.
+
+  Note that using the primary goal facts in the same manner as the
+  method arguments obtained via concrete syntax or the context does
+  not meet the requirement of ``strong emphasis on facts'' of regular
+  proof methods, because rewrite rules as used above can be easily
+  ignored.  A proof text ``\hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}~\isa{foo}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{my{\isacharunderscore}simp}'' where \isa{foo} is not used would
+  deceive the reader.
+
+  \medskip The technical treatment of rules from the context requires
+  further attention.  Above we rebuild a fresh \verb|simpset| from
+  the arguments and \emph{all} rules retrieved from the context on
+  every invocation of the method.  This does not scale to really large
+  collections of rules, which easily emerges in the context of a big
+  theory library, for example.
+
+  This is an inherent limitation of the simplistic rule management via
+  functor \verb|Named_Thms|, because it lacks tool-specific
+  storage and retrieval.  More realistic applications require
+  efficient index-structures that organize theorems in a customized
+  manner, such as a discrimination net that is indexed by the
+  left-hand sides of rewrite rules.  For variations on the Simplifier,
+  re-use of the existing type \verb|simpset| is adequate, but
+  scalability requires it be maintained statically within the context
+  data, not dynamically on each tool invocation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Attributes \label{sec:attributes}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+An \emph{attribute} is a function \isa{context\ {\isasymtimes}\ thm\ {\isasymrightarrow}\ context\ {\isasymtimes}\ thm}, which means both a (generic) context and a theorem
+  can be modified simultaneously.  In practice this fully general form
+  is very rare, instead attributes are presented either as
+  \emph{declaration attribute:} \isa{thm\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} or
+  \emph{rule attribute:} \isa{context\ {\isasymrightarrow}\ thm\ {\isasymrightarrow}\ thm}.
+
+  Attributes can have additional arguments via concrete syntax.  There
+  is a collection of context-sensitive parsers for various logical
+  entities (types, terms, theorems).  These already take care of
+  applying morphisms to the arguments when attribute expressions are
+  moved into a different context (see also \secref{sec:morphisms}).
+
+  When implementing declaration attributes, it is important to operate
+  exactly on the variant of the generic context that is provided by
+  the system, which is either global theory context or local proof
+  context.  In particular, the background theory of a local context
+  must not be modified in this situation!%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{attribute}\verb|type attribute = Context.generic * thm -> Context.generic * thm| \\
+  \indexdef{}{ML}{Thm.rule\_attribute}\verb|Thm.rule_attribute: (Context.generic -> thm -> thm) -> attribute| \\
+  \indexdef{}{ML}{Thm.declaration\_attribute}\verb|Thm.declaration_attribute: |\isasep\isanewline%
+\verb|  (thm -> Context.generic -> Context.generic) -> attribute| \\
+  \indexdef{}{ML}{Attrib.setup}\verb|Attrib.setup: binding -> attribute context_parser ->|\isasep\isanewline%
+\verb|  string -> theory -> theory| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type \verb|attribute| represents attributes as concrete
+  type alias.
+
+  \item \verb|Thm.rule_attribute|~\isa{{\isacharparenleft}fn\ context\ {\isacharequal}{\isachargreater}\ rule{\isacharparenright}} wraps
+  a context-dependent rule (mapping on \verb|thm|) as attribute.
+
+  \item \verb|Thm.declaration_attribute|~\isa{{\isacharparenleft}fn\ thm\ {\isacharequal}{\isachargreater}\ decl{\isacharparenright}}
+  wraps a theorem-dependent declaration (mapping on \verb|Context.generic|) as attribute.
+
+  \item \verb|Attrib.setup|~\isa{name\ parser\ description} provides
+  the functionality of the Isar command \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}} as
+  ML function.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+See also \hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}} in
+  \cite{isabelle-isar-ref} which includes some abstract examples.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
 \isadelimtheory
 %
 \endisadelimtheory