# HG changeset patch
# User wenzelm
# Date 1235837313 -3600
# Node ID 5989863ffafc3e0432f30647dfc24099f0b86ef2
# Parent  b533ef41b11e002250d211b1ced367dae9c7466d
added method "coherent";
tuned formal markup;

diff -r b533ef41b11e -r 5989863ffafc doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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 {*