1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 17:08:08 2009 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 17:08:33 2009 +0100
1.3 @@ -775,7 +775,7 @@
1.4
1.5 text {*
1.6 \begin{matharray}{rcl}
1.7 - @{method_def (HOL) "iprover"} & : & @{text method} \\
1.8 + @{method_def (HOL) iprover} & : & @{text method} \\
1.9 \end{matharray}
1.10
1.11 \begin{rail}
1.12 @@ -783,11 +783,11 @@
1.13 ;
1.14 \end{rail}
1.15
1.16 - The @{method iprover} method performs intuitionistic proof search,
1.17 - depending on specifically declared rules from the context, or given
1.18 - as explicit arguments. Chained facts are inserted into the goal
1.19 - before commencing proof search; ``@{method iprover}@{text "!"}''
1.20 - means to include the current @{fact prems} as well.
1.21 + The @{method (HOL) iprover} method performs intuitionistic proof
1.22 + search, depending on specifically declared rules from the context,
1.23 + or given as explicit arguments. Chained facts are inserted into the
1.24 + goal before commencing proof search; ``@{method (HOL) iprover}@{text
1.25 + "!"}'' means to include the current @{fact prems} as well.
1.26
1.27 Rules need to be classified as @{attribute (Pure) intro},
1.28 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
1.29 @@ -800,6 +800,26 @@
1.30 *}
1.31
1.32
1.33 +section {* Coherent Logic *}
1.34 +
1.35 +text {*
1.36 + \begin{matharray}{rcl}
1.37 + @{method_def (HOL) "coherent"} & : & @{text method} \\
1.38 + \end{matharray}
1.39 +
1.40 + \begin{rail}
1.41 + 'coherent' thmrefs?
1.42 + ;
1.43 + \end{rail}
1.44 +
1.45 + The @{method (HOL) coherent} method solves problems of
1.46 + \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
1.47 + applications in confluence theory, lattice theory and projective
1.48 + geometry. See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
1.49 + examples.
1.50 +*}
1.51 +
1.52 +
1.53 section {* Invoking automated reasoning tools -- The Sledgehammer *}
1.54
1.55 text {*