# HG changeset patch
# User wenzelm
# Date 1235837372 -3600
# Node ID afdf7808cfd0d36b11cbd360155233c28a5e8bb1
# Parent  5989863ffafc3e0432f30647dfc24099f0b86ef2
updated generated files;

diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Document{\isacharunderscore}Preparation}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Generic}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -779,6 +779,58 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Intuitionistic proof search%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
+  \end{matharray}
+
+  \begin{rail}
+    'iprover' ('!' ?) (rulemod *)
+    ;
+  \end{rail}
+
+  The \hyperlink{method.HOL.iprover}{\mbox{\isa{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; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
+  
+  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
+  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
+  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
+  applied aggressively (without considering back-tracking later).
+  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
+  single-step \hyperlink{method.rule}{\mbox{\isa{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.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Coherent Logic%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
+  \end{matharray}
+
+  \begin{rail}
+    'coherent' thmrefs?
+    ;
+  \end{rail}
+
+  The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
+  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
+  applications in confluence theory, lattice theory and projective
+  geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Coherent{\isachardot}thy}}}} for some
+  examples.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
 }
 \isamarkuptrue%
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/ML_Tactic.tex
--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{ML{\isacharunderscore}Tactic}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Misc}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Outer{\isacharunderscore}Syntax}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -693,7 +693,6 @@
     \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
     \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
     \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
-    \indexdef{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\[0.5ex]
     \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
     \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
     \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
@@ -708,8 +707,6 @@
     ;
     'rule' thmrefs?
     ;
-    'iprover' ('!' ?) (rulemod *)
-    ;
     rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
     ;
     ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
@@ -764,26 +761,11 @@
   default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' 
   (double-dot) steps (see \secref{sec:proof-steps}).
   
-  \item \hyperlink{method.iprover}{\mbox{\isa{iprover}}} 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; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
-  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
-  
-  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
-  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
-  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
-  applied aggressively (without considering back-tracking later).
-  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
-  single-step \hyperlink{method.rule}{\mbox{\isa{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.
-  
   \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
-  destruct rules, to be used with the \hyperlink{method.rule}{\mbox{\isa{rule}}} and \hyperlink{method.iprover}{\mbox{\isa{iprover}}} methods.  Note that the latter will ignore rules declared
-  with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most
-  aggressively.
+  destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
+  tools.  Note that the latter will ignore rules declared with
+  ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most aggressively.
   
   The classical reasoner (see \secref{sec:classical}) introduces its
   own variants of these attributes; use qualified names to access the
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Quick_Reference.tex
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Quick{\isacharunderscore}Reference}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/Symbols.tex
--- a/doc-src/IsarRef/Thy/document/Symbols.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Symbols}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
diff -r 5989863ffafc -r afdf7808cfd0 doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{ZF{\isacharunderscore}Specific}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %