--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon May 02 20:34:34 2011 +0200
@@ -399,7 +399,7 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, @{antiquotation_option_def source}~@{text "= true"}
+ In contrast, @{antiquotation_option source}~@{text "= true"}
admits direct printing of the given source text, with the desirable
well-formedness check in the background, but without modification of
the printed text.
--- a/doc-src/IsarRef/Thy/Framework.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy Mon May 02 20:34:34 2011 +0200
@@ -521,23 +521,23 @@
"then"} or @{command using}, and then operate on the goal state.
Some basic methods are predefined: ``@{method "-"}'' leaves the goal
unchanged, ``@{method this}'' applies the facts as rules to the
- goal, ``@{method "rule"}'' applies the facts to another rule and the
- result to the goal (both ``@{method this}'' and ``@{method rule}''
+ goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
+ result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
refer to @{inference resolution} of
\secref{sec:framework-resolution}). The secondary arguments to
- ``@{method rule}'' may be specified explicitly as in ``@{text "(rule
+ ``@{method (Pure) rule}'' may be specified explicitly as in ``@{text "(rule
a)"}'', or picked from the context. In the latter case, the system
first tries rules declared as @{attribute (Pure) elim} or
@{attribute (Pure) dest}, followed by those declared as @{attribute
(Pure) intro}.
- The default method for @{command proof} is ``@{method rule}''
+ The default method for @{command proof} is ``@{method (Pure) rule}''
(arguments picked from the context), for @{command qed} it is
``@{method "-"}''. Further abbreviations for terminal proof steps
are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text
"method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command
- "by"}~@{method rule}, and ``@{command "."}'' for ``@{command
+ "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command
"by"}~@{method this}''. The @{command unfolding} element operates
directly on the current facts and goal by applying equalities.
--- a/doc-src/IsarRef/Thy/Generic.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon May 02 20:34:34 2011 +0200
@@ -795,7 +795,7 @@
premises of a sub-goal, using the meta-level equations declared via
@{attribute atomize} (as an attribute) beforehand. As a result,
heavily nested goals become amenable to fundamental operations such
- as resolution (cf.\ the @{method rule} method). Giving the ``@{text
+ as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text
"(full)"}'' option here means to turn the whole subgoal into an
object-statement (if possible), including the outermost parameters
and assumptions as well.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon May 02 20:34:34 2011 +0200
@@ -896,7 +896,7 @@
``@{text "!"}'' indicator refers to ``safe'' rules, which may be
applied aggressively (without considering back-tracking later).
Rules declared with ``@{text "?"}'' are ignored in proof search (the
- single-step @{method rule} method still observes these). An
+ single-step @{method (Pure) rule} method still observes these). An
explicit weight annotation may be given as well; otherwise the
number of rule premises will be taken into account here.
*}
@@ -1419,7 +1419,7 @@
@{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
- @{attribute_def (HOL) code} & : & @{text attribute} \\
+ @{attribute_def code} & : & @{text attribute} \\
\end{matharray}
@{rail "
@@ -1452,7 +1452,7 @@
attachment: 'attach' modespec? '{' @{syntax text} '}'
;
- @@{attribute (HOL) code} (name)?
+ @@{attribute code} name?
"}
*}
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Mon May 02 20:34:34 2011 +0200
@@ -51,11 +51,10 @@
\secref{sec:tactics}) would be sufficient to cover the four modes,
either with or without instantiation, and either with single or
multiple arguments. Although it is more convenient in most cases to
- use the plain @{method rule} method (see
- \secref{sec:pure-meth-att}), or any of its ``improper'' variants
- @{method erule}, @{method drule}, @{method frule} (see
- \secref{sec:misc-meth-att}). Note that explicit goal addressing is
- only supported by the actual @{method rule_tac} version.
+ use the plain @{method_ref (Pure) rule} method, or any of its
+ ``improper'' variants @{method erule}, @{method drule}, @{method
+ frule}. Note that explicit goal addressing is only supported by the
+ actual @{method rule_tac} version.
With this in mind, plain resolution tactics correspond to Isar
methods as follows.
--- a/doc-src/IsarRef/Thy/Proof.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon May 02 20:34:34 2011 +0200
@@ -339,7 +339,7 @@
facts in order to establish the goal to be claimed next. The
initial proof method invoked to refine that will be offered the
facts to do ``anything appropriate'' (see also
- \secref{sec:proof-steps}). For example, method @{method_ref rule}
+ \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
(see \secref{sec:pure-meth-att}) would typically do an elimination
rather than an introduction. Automatic methods usually insert the
facts into the goal state before operation. This provides a simple
@@ -368,7 +368,7 @@
effect apart from entering @{text "prove(chain)"} mode, since
@{fact_ref nothing} is bound to the empty list of theorems.
- Basic proof methods (such as @{method_ref rule}) expect multiple
+ Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
facts to be given in their proper order, corresponding to a prefix
of the premises of the rule involved. Note that positions may be
easily skipped using something like @{command "from"}~@{text "_
@@ -618,10 +618,11 @@
an intelligible manner.
Unless given explicitly by the user, the default initial method is
- ``@{method_ref rule}'', which applies a single standard elimination
- or introduction rule according to the topmost symbol involved.
- There is no separate default terminal method. Any remaining goals
- are always solved by assumption in the very last step.
+ @{method_ref (Pure) rule} (or its classical variant @{method_ref
+ rule}), which applies a single standard elimination or introduction
+ rule according to the topmost symbol involved. There is no separate
+ default terminal method. Any remaining goals are always solved by
+ assumption in the very last step.
@{rail "
@@{command proof} method?
@@ -697,11 +698,11 @@
@{method_def "fact"} & : & @{text method} \\
@{method_def "assumption"} & : & @{text method} \\
@{method_def "this"} & : & @{text method} \\
- @{method_def "rule"} & : & @{text method} \\
+ @{method_def (Pure) "rule"} & : & @{text method} \\
@{attribute_def (Pure) "intro"} & : & @{text attribute} \\
@{attribute_def (Pure) "elim"} & : & @{text attribute} \\
@{attribute_def (Pure) "dest"} & : & @{text attribute} \\
- @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
+ @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]
@{attribute_def "OF"} & : & @{text attribute} \\
@{attribute_def "of"} & : & @{text attribute} \\
@{attribute_def "where"} & : & @{text attribute} \\
@@ -710,7 +711,7 @@
@{rail "
@@{method fact} @{syntax thmrefs}?
;
- @@{method rule} @{syntax thmrefs}?
+ @@{method (Pure) rule} @{syntax thmrefs}?
;
rulemod: ('intro' | 'elim' | 'dest')
((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
@@ -718,7 +719,7 @@
(@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
('!' | () | '?') @{syntax nat}?
;
- @@{attribute rule} 'del'
+ @@{attribute (Pure) rule} 'del'
;
@@{attribute OF} @{syntax thmrefs}
;
@@ -734,7 +735,7 @@
\item ``@{method "-"}'' (minus) does nothing but insert the forward
chaining facts as premises into the goal. Note that command
@{command_ref "proof"} without any method actually performs a single
- reduction step using the @{method_ref rule} method; thus a plain
+ reduction step using the @{method_ref (Pure) rule} method; thus a plain
\emph{do-nothing} proof step would be ``@{command "proof"}~@{text
"-"}'' rather than @{command "proof"} alone.
@@ -761,12 +762,12 @@
rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
"by"}~@{text this}''.
- \item @{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
+ \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
argument in backward manner; facts are used to reduce the rule
- before applying it to the goal. Thus @{method rule} without facts
+ before applying it to the goal. Thus @{method (Pure) rule} without facts
is plain introduction, while with facts it becomes elimination.
- When no arguments are given, the @{method rule} method tries to pick
+ When no arguments are given, the @{method (Pure) rule} method tries to pick
appropriate rules automatically, as declared in the current context
using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
@{attribute (Pure) dest} attributes (see below). This is the
@@ -775,7 +776,7 @@
\item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
@{attribute (Pure) dest} declare introduction, elimination, and
- destruct rules, to be used with method @{method rule}, and similar
+ destruct rules, to be used with method @{method (Pure) rule}, and similar
tools. Note that the latter will ignore rules declared with
``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
@@ -784,7 +785,7 @@
present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
"Pure.intro"}.
- \item @{attribute rule}~@{text del} undeclares introduction,
+ \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
elimination, or destruct rules.
\item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
--- a/doc-src/IsarRef/Thy/Spec.thy Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon May 02 20:34:34 2011 +0200
@@ -631,7 +631,7 @@
@{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
@{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon May 02 20:34:34 2011 +0200
@@ -553,7 +553,7 @@
not under direct control of the author, it may even fluctuate a bit
as the underlying theory is changed later on.
- In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}}
+ In contrast, \hyperlink{antiquotation option.source}{\mbox{\isa{source}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}}
admits direct printing of the given source text, with the desirable
well-formedness check in the background, but without modification of
the printed text.
--- a/doc-src/IsarRef/Thy/document/Framework.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Mon May 02 20:34:34 2011 +0200
@@ -632,19 +632,19 @@
populated later. Methods use the facts indicated by \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, and then operate on the goal state.
Some basic methods are predefined: ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' leaves the goal
unchanged, ``\hyperlink{method.this}{\mbox{\isa{this}}}'' applies the facts as rules to the
- goal, ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' applies the facts to another rule and the
- result to the goal (both ``\hyperlink{method.this}{\mbox{\isa{this}}}'' and ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
+ goal, ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}'' applies the facts to another rule and the
+ result to the goal (both ``\hyperlink{method.this}{\mbox{\isa{this}}}'' and ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}''
refer to \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} of
\secref{sec:framework-resolution}). The secondary arguments to
- ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' may be specified explicitly as in ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'', or picked from the context. In the latter case, the system
+ ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}'' may be specified explicitly as in ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'', or picked from the context. In the latter case, the system
first tries rules declared as \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}} or
\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}, followed by those declared as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}.
- The default method for \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} is ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
+ The default method for \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} is ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}''
(arguments picked from the context), for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} it is
``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}''. Further abbreviations for terminal proof steps
are ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'' for
- ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'', and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.rule}{\mbox{\isa{rule}}}, and ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.this}{\mbox{\isa{this}}}''. The \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} element operates
+ ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'', and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.this}{\mbox{\isa{this}}}''. The \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} element operates
directly on the current facts and goal by applying equalities.
\medskip Block structure can be indicated explicitly by ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isaliteral{7D}{\isacharbraceright}}}}}}'', although the body of a sub-proof
--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon May 02 20:34:34 2011 +0200
@@ -1286,7 +1286,7 @@
premises of a sub-goal, using the meta-level equations declared via
\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand. As a result,
heavily nested goals become amenable to fundamental operations such
- as resolution (cf.\ the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). Giving the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}full{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option here means to turn the whole subgoal into an
+ as resolution (cf.\ the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method). Giving the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}full{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option here means to turn the whole subgoal into an
object-statement (if possible), including the outermost parameters
and assumptions as well.
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 20:34:34 2011 +0200
@@ -1230,7 +1230,7 @@
``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be
applied aggressively (without considering back-tracking later).
Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the
- single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these). An
+ single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An
explicit weight annotation may be given as well; otherwise the
number of rule premises will be taken into account here.%
\end{isamarkuptext}%
@@ -2167,7 +2167,7 @@
\indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
\end{matharray}
\begin{railoutput}
@@ -2272,7 +2272,7 @@
\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
\rail@end
\rail@begin{2}{\isa{}}
-\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
+\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{name}}[]
--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Mon May 02 20:34:34 2011 +0200
@@ -70,11 +70,9 @@
\secref{sec:tactics}) would be sufficient to cover the four modes,
either with or without instantiation, and either with single or
multiple arguments. Although it is more convenient in most cases to
- use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see
- \secref{sec:pure-meth-att}), or any of its ``improper'' variants
- \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see
- \secref{sec:misc-meth-att}). Note that explicit goal addressing is
- only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version.
+ use the plain \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method, or any of its
+ ``improper'' variants \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}}. Note that explicit goal addressing is only supported by the
+ actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version.
With this in mind, plain resolution tactics correspond to Isar
methods as follows.
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 20:34:34 2011 +0200
@@ -445,7 +445,7 @@
facts in order to establish the goal to be claimed next. The
initial proof method invoked to refine that will be offered the
facts to do ``anything appropriate'' (see also
- \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
+ \secref{sec:proof-steps}). For example, method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}
(see \secref{sec:pure-meth-att}) would typically do an elimination
rather than an introduction. Automatic methods usually insert the
facts into the goal state before operation. This provides a simple
@@ -472,7 +472,7 @@
effect apart from entering \isa{{\isaliteral{22}{\isachardoublequote}}prove{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode, since
\indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
- Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
+ Basic proof methods (such as \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}) expect multiple
facts to be given in their proper order, corresponding to a prefix
of the premises of the rule involved. Note that positions may be
easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ b{\isaliteral{22}{\isachardoublequote}}}, for example. This involves the trivial rule
@@ -843,10 +843,10 @@
an intelligible manner.
Unless given explicitly by the user, the default initial method is
- ``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
- or introduction rule according to the topmost symbol involved.
- There is no separate default terminal method. Any remaining goals
- are always solved by assumption in the very last step.
+ \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} (or its classical variant \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}), which applies a single standard elimination or introduction
+ rule according to the topmost symbol involved. There is no separate
+ default terminal method. Any remaining goals are always solved by
+ assumption in the very last step.
\begin{railoutput}
\rail@begin{2}{\isa{}}
@@ -943,11 +943,11 @@
\indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
\indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
\indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
- \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
+ \indexdef{Pure}{method}{rule}\hypertarget{method.Pure.rule}{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
\indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
\indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
\indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
+ \indexdef{Pure}{attribute}{rule}\hypertarget{attribute.Pure.rule}{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
\indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
@@ -962,7 +962,7 @@
\rail@endbar
\rail@end
\rail@begin{2}{\isa{}}
-\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
@@ -1013,7 +1013,7 @@
\rail@endbar
\rail@end
\rail@begin{1}{\isa{}}
-\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
+\rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
\rail@term{\isa{del}}[]
\rail@end
\rail@begin{1}{\isa{}}
@@ -1063,7 +1063,7 @@
\item ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' (minus) does nothing but insert the forward
chaining facts as premises into the goal. Note that command
\indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
- reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
+ reduction step using the \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method; thus a plain
\emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
\item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} composes some fact from
@@ -1086,12 +1086,12 @@
\item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
rules. Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
- \item \hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
+ \item \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
argument in backward manner; facts are used to reduce the rule
- before applying it to the goal. Thus \hyperlink{method.rule}{\mbox{\isa{rule}}} without facts
+ before applying it to the goal. Thus \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} without facts
is plain introduction, while with facts it becomes elimination.
- When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
+ When no arguments are given, the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method tries to pick
appropriate rules automatically, as declared in the current context
using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below). This is the
@@ -1100,7 +1100,7 @@
\item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
- destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
+ destruct rules, to be used with method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and similar
tools. Note that the latter will ignore rules declared with
``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'', while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' are used most aggressively.
@@ -1108,7 +1108,7 @@
own variants of these attributes; use qualified names to access the
present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}intro}}}.
- \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
+ \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
elimination, or destruct rules.
\item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon May 02 20:34:34 2011 +0200
@@ -957,7 +957,7 @@
\indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\