--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 17:08:08 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 17:08:33 2009 +0100
@@ -775,7 +775,7 @@
text {*
\begin{matharray}{rcl}
- @{method_def (HOL) "iprover"} & : & @{text method} \\
+ @{method_def (HOL) iprover} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -783,11 +783,11 @@
;
\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.
+ The @{method (HOL) 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 (HOL) 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
@@ -800,6 +800,26 @@
*}
+section {* Coherent Logic *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def (HOL) "coherent"} & : & @{text method} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'coherent' thmrefs?
+ ;
+ \end{rail}
+
+ The @{method (HOL) coherent} method solves problems of
+ \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
+ applications in confluence theory, lattice theory and projective
+ geometry. See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
+ examples.
+*}
+
+
section {* Invoking automated reasoning tools -- The Sledgehammer *}
text {*