--- 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 {*