# HG changeset patch
# User blanchet
# Date 1309179397 -7200
# Node ID 36ba44fe07810b69e60e09689c5f406e1270beb7
# Parent  78c2f14b35df7bdb98807904d72fd2c897104739
document "meson" and "metis" in HOL specific section of the Isar ref manual

diff -r 78c2f14b35df -r 36ba44fe0781 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 27 14:56:35 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 27 14:56:37 2011 +0200
@@ -1287,6 +1287,33 @@
   number of rule premises will be taken into account here.
 *}
 
+section {* Model Elimination and Resolution *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{method_def (HOL) "meson"} & : & @{text method} \\
+    @{method_def (HOL) "metis"} & : & @{text method} \\
+  \end{matharray}
+
+  @{rail "
+    @@{method (HOL) meson} @{syntax thmrefs}?
+    ;
+
+    @@{method (HOL) metis} ( '(' ('partial_types' | 'full_types' | 'no_types'
+                                  | @{syntax name}) ')' )? @{syntax thmrefs}?
+  "}
+
+  The @{method (HOL) meson} method implements Loveland's model elimination
+  procedure \cite{loveland-78}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
+  examples.
+
+  The @{method (HOL) metis} method combines ordered resolution and ordered
+  paramodulation to find first-order (or mildly higher-order) proofs. The first
+  optional argument specifies a type encoding; see the Sledgehammer manual
+  \cite{isabelle-sledgehammer} for details. The @{file
+  "~~/src/HOL/Metis_Examples"} directory contains several small theories
+  developed to a large extent using Metis.
+*}
 
 section {* Coherent Logic *}
 
diff -r 78c2f14b35df -r 36ba44fe0781 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 27 14:56:35 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 27 14:56:37 2011 +0200
@@ -1816,6 +1816,60 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Model Elimination and Resolution%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{HOL}{method}{meson}\hypertarget{method.HOL.meson}{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}} & : & \isa{method} \\
+    \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
+  \end{matharray}
+
+  \begin{railoutput}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.HOL.meson}{\mbox{\isa{meson}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{5}{}
+\rail@term{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@bar
+\rail@term{\isa{partial{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{2}
+\rail@term{\isa{full{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{3}
+\rail@term{\isa{no{\isaliteral{5F}{\isacharunderscore}}types}}[]
+\rail@nextbar{4}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@endbar
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+  The \hyperlink{method.HOL.meson}{\mbox{\isa{meson}}} method implements Loveland's model elimination
+  procedure \cite{loveland-78}. See \verb|~~/src/HOL/ex/Meson_Test.thy| for
+  examples.
+
+  The \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}} method combines ordered resolution and ordered
+  paramodulation to find first-order (or mildly higher-order) proofs. The first
+  optional argument specifies a type encoding; see the Sledgehammer manual
+  \cite{isabelle-sledgehammer} for details. The \verb|~~/src/HOL/Metis_Examples| directory contains several small theories
+  developed to a large extent using Metis.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Coherent Logic%
 }
 \isamarkuptrue%