# HG changeset patch
# User wenzelm
# Date 1235836107 -3600
# Node ID 9531eaafd781b41c40c126009c2fcb1dce475345
# Parent  9a20be5be90bccef33226a9b8dffb1fa06cb88b5
moved method "iprover" to HOL specific part;

diff -r 9a20be5be90b -r 9531eaafd781 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Feb 28 16:39:46 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Feb 28 16:48:27 2009 +0100
@@ -771,6 +771,35 @@
 *}
 
 
+section {* Intuitionistic proof search *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "iprover"} & : & @{text method} \\
+  \end{matharray}
+
+  \begin{rail}
+    'iprover' ('!' ?) (rulemod *)
+    ;
+  \end{rail}
+
+  The @{method iprover} method 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; ``@{method iprover}@{text "!"}''
+  means to include the current @{fact prems} as well.
+  
+  Rules need to be classified as @{attribute (Pure) intro},
+  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
+  ``@{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
+  explicit weight annotation may be given as well; otherwise the
+  number of rule premises will be taken into account here.
+*}
+
+
 section {* Invoking automated reasoning tools -- The Sledgehammer *}
 
 text {*
diff -r 9a20be5be90b -r 9531eaafd781 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Sat Feb 28 16:39:46 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Sat Feb 28 16:48:27 2009 +0100
@@ -683,7 +683,6 @@
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
     @{method_def "rule"} & : & @{text method} \\
-    @{method_def "iprover"} & : & @{text method} \\[0.5ex]
     @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
     @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
     @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
@@ -698,8 +697,6 @@
     ;
     'rule' thmrefs?
     ;
-    'iprover' ('!' ?) (rulemod *)
-    ;
     rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
     ;
     ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
@@ -758,27 +755,11 @@
   default behavior of @{command "proof"} and ``@{command ".."}'' 
   (double-dot) steps (see \secref{sec:proof-steps}).
   
-  \item @{method 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; ``@{method iprover}@{text "!"}''
-  means to include the current @{fact prems} as well.
-  
-  Rules need to be classified as @{attribute (Pure) intro},
-  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
-  ``@{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
-  explicit weight annotation may be given as well; otherwise the
-  number of rule premises will be taken into account here.
-  
   \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
   @{attribute (Pure) dest} declare introduction, elimination, and
-  destruct rules, to be used with the @{method rule} and @{method
-  iprover} methods.  Note that the latter will ignore rules declared
-  with ``@{text "?"}'', while ``@{text "!"}''  are used most
-  aggressively.
+  destruct rules, to be used with method @{method rule}, and similar
+  tools.  Note that the latter will ignore rules declared with
+  ``@{text "?"}'', while ``@{text "!"}''  are used most aggressively.
   
   The classical reasoner (see \secref{sec:classical}) introduces its
   own variants of these attributes; use qualified names to access the