# HG changeset patch
# User wenzelm
# Date 1127482362 -7200
# Node ID 4da04f70221f2265f34b86594a3517d6f493a774
# Parent  7540ccd2b44555199f87cb822a71e915cb276509
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;

diff -r 7540ccd2b445 -r 4da04f70221f doc-src/IsarRef/pure.tex
--- 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.