--- a/doc-src/IsarRef/Thy/document/Proof.tex Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Sat Feb 28 17:09:32 2009 +0100
@@ -693,7 +693,6 @@
\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{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\[0.5ex]
\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} \\
@@ -708,8 +707,6 @@
;
'rule' thmrefs?
;
- 'iprover' ('!' ?) (rulemod *)
- ;
rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
;
('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
@@ -764,26 +761,11 @@
default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}''
(double-dot) steps (see \secref{sec:proof-steps}).
- \item \hyperlink{method.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search,
- depending on specifically declared rules from the context, or given
- as explicit arguments. Chained facts are inserted into the goal
- before commencing proof search; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
- means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
-
- Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
- \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
- ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
- applied aggressively (without considering back-tracking later).
- Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
- single-step \hyperlink{method.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.
-
\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 the \hyperlink{method.rule}{\mbox{\isa{rule}}} and \hyperlink{method.iprover}{\mbox{\isa{iprover}}} methods. Note that the latter will ignore rules declared
- with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most
- aggressively.
+ destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
+ tools. Note that the latter will ignore rules declared with
+ ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most aggressively.
The classical reasoner (see \secref{sec:classical}) introduces its
own variants of these attributes; use qualified names to access the