--- a/doc-src/IsarRef/pure.tex Fri Sep 23 14:55:28 2005 +0200
+++ b/doc-src/IsarRef/pure.tex Fri Sep 23 15:32:42 2005 +0200
@@ -1027,7 +1027,7 @@
\ref{ch:logics}).
\indexisarmeth{$-$}\indexisarmeth{assumption}
-\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
+\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{iprover}
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
@@ -1036,7 +1036,7 @@
assumption & : & \isarmeth \\
this & : & \isarmeth \\
rule & : & \isarmeth \\
- rules & : & \isarmeth \\[0.5ex]
+ iprover & : & \isarmeth \\[0.5ex]
intro & : & \isaratt \\
elim & : & \isaratt \\
dest & : & \isaratt \\
@@ -1049,7 +1049,7 @@
\begin{rail}
'rule' thmrefs?
;
- 'rules' ('!' ?) (rulemod *)
+ 'iprover' ('!' ?) (rulemod *)
;
rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
;
@@ -1094,10 +1094,10 @@
$\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
\S\ref{sec:proof-steps}).
-\item [$rules$] performs intuitionistic proof search, depending on
+\item [$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; ``$rules!$'' means to include the current $prems$ as well.
+ search; ``$iprover!$'' means to include the current $prems$ as well.
Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
indicator refers to ``safe'' rules, which may be applied aggressively
@@ -1107,7 +1107,7 @@
number of rule premises will be taken into account here.
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
- destruct rules, to be used with the $rule$ and $rules$ methods. Note that
+ destruct rules, to be used with the $rule$ and $iprover$ methods. Note that
the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
most aggressively.