updated generated files;
authorwenzelm
Sat Feb 28 17:09:32 2009 +0100 (2009-02-28)
changeset 30172afdf7808cfd0
parent 30171 5989863ffafc
child 30173 eabece26b89b
child 30176 78610979b3c6
updated generated files;
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/ML_Tactic.tex
doc-src/IsarRef/Thy/document/Misc.tex
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
doc-src/IsarRef/Thy/document/Proof.tex
doc-src/IsarRef/Thy/document/Quick_Reference.tex
doc-src/IsarRef/Thy/document/Symbols.tex
doc-src/IsarRef/Thy/document/ZF_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Feb 28 17:08:33 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Feb 28 17:09:32 2009 +0100
     1.3 @@ -3,8 +3,6 @@
     1.4  \def\isabellecontext{Document{\isacharunderscore}Preparation}%
     1.5  %
     1.6  \isadelimtheory
     1.7 -\isanewline
     1.8 -\isanewline
     1.9  %
    1.10  \endisadelimtheory
    1.11  %
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Feb 28 17:08:33 2009 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Feb 28 17:09:32 2009 +0100
     2.3 @@ -3,8 +3,6 @@
     2.4  \def\isabellecontext{Generic}%
     2.5  %
     2.6  \isadelimtheory
     2.7 -\isanewline
     2.8 -\isanewline
     2.9  %
    2.10  \endisadelimtheory
    2.11  %
     3.1 --- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
     3.3 @@ -3,8 +3,6 @@
     3.4  \def\isabellecontext{HOLCF{\isacharunderscore}Specific}%
     3.5  %
     3.6  \isadelimtheory
     3.7 -\isanewline
     3.8 -\isanewline
     3.9  %
    3.10  \endisadelimtheory
    3.11  %
     4.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
     4.3 @@ -779,6 +779,58 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  %
     4.7 +\isamarkupsection{Intuitionistic proof search%
     4.8 +}
     4.9 +\isamarkuptrue%
    4.10 +%
    4.11 +\begin{isamarkuptext}%
    4.12 +\begin{matharray}{rcl}
    4.13 +    \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
    4.14 +  \end{matharray}
    4.15 +
    4.16 +  \begin{rail}
    4.17 +    'iprover' ('!' ?) (rulemod *)
    4.18 +    ;
    4.19 +  \end{rail}
    4.20 +
    4.21 +  The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
    4.22 +  search, depending on specifically declared rules from the context,
    4.23 +  or given as explicit arguments.  Chained facts are inserted into the
    4.24 +  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.
    4.25 +  
    4.26 +  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
    4.27 +  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
    4.28 +  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
    4.29 +  applied aggressively (without considering back-tracking later).
    4.30 +  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
    4.31 +  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
    4.32 +  explicit weight annotation may be given as well; otherwise the
    4.33 +  number of rule premises will be taken into account here.%
    4.34 +\end{isamarkuptext}%
    4.35 +\isamarkuptrue%
    4.36 +%
    4.37 +\isamarkupsection{Coherent Logic%
    4.38 +}
    4.39 +\isamarkuptrue%
    4.40 +%
    4.41 +\begin{isamarkuptext}%
    4.42 +\begin{matharray}{rcl}
    4.43 +    \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
    4.44 +  \end{matharray}
    4.45 +
    4.46 +  \begin{rail}
    4.47 +    'coherent' thmrefs?
    4.48 +    ;
    4.49 +  \end{rail}
    4.50 +
    4.51 +  The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
    4.52 +  \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
    4.53 +  applications in confluence theory, lattice theory and projective
    4.54 +  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
    4.55 +  examples.%
    4.56 +\end{isamarkuptext}%
    4.57 +\isamarkuptrue%
    4.58 +%
    4.59  \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
    4.60  }
    4.61  \isamarkuptrue%
     5.1 --- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Feb 28 17:08:33 2009 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Feb 28 17:09:32 2009 +0100
     5.3 @@ -3,8 +3,6 @@
     5.4  \def\isabellecontext{ML{\isacharunderscore}Tactic}%
     5.5  %
     5.6  \isadelimtheory
     5.7 -\isanewline
     5.8 -\isanewline
     5.9  %
    5.10  \endisadelimtheory
    5.11  %
     6.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex	Sat Feb 28 17:08:33 2009 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Sat Feb 28 17:09:32 2009 +0100
     6.3 @@ -3,8 +3,6 @@
     6.4  \def\isabellecontext{Misc}%
     6.5  %
     6.6  \isadelimtheory
     6.7 -\isanewline
     6.8 -\isanewline
     6.9  %
    6.10  \endisadelimtheory
    6.11  %
     7.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Feb 28 17:08:33 2009 +0100
     7.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Feb 28 17:09:32 2009 +0100
     7.3 @@ -3,8 +3,6 @@
     7.4  \def\isabellecontext{Outer{\isacharunderscore}Syntax}%
     7.5  %
     7.6  \isadelimtheory
     7.7 -\isanewline
     7.8 -\isanewline
     7.9  %
    7.10  \endisadelimtheory
    7.11  %
     8.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Sat Feb 28 17:08:33 2009 +0100
     8.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Sat Feb 28 17:09:32 2009 +0100
     8.3 @@ -693,7 +693,6 @@
     8.4      \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
     8.5      \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
     8.6      \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
     8.7 -    \indexdef{}{method}{iprover}\hypertarget{method.iprover}{\hyperlink{method.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\[0.5ex]
     8.8      \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
     8.9      \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
    8.10      \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
    8.11 @@ -708,8 +707,6 @@
    8.12      ;
    8.13      'rule' thmrefs?
    8.14      ;
    8.15 -    'iprover' ('!' ?) (rulemod *)
    8.16 -    ;
    8.17      rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
    8.18      ;
    8.19      ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
    8.20 @@ -764,26 +761,11 @@
    8.21    default behavior of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' 
    8.22    (double-dot) steps (see \secref{sec:proof-steps}).
    8.23    
    8.24 -  \item \hyperlink{method.iprover}{\mbox{\isa{iprover}}} performs intuitionistic proof search,
    8.25 -  depending on specifically declared rules from the context, or given
    8.26 -  as explicit arguments.  Chained facts are inserted into the goal
    8.27 -  before commencing proof search; ``\hyperlink{method.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
    8.28 -  means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
    8.29 -  
    8.30 -  Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
    8.31 -  \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
    8.32 -  ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
    8.33 -  applied aggressively (without considering back-tracking later).
    8.34 -  Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
    8.35 -  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
    8.36 -  explicit weight annotation may be given as well; otherwise the
    8.37 -  number of rule premises will be taken into account here.
    8.38 -  
    8.39    \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
    8.40    \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
    8.41 -  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
    8.42 -  with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most
    8.43 -  aggressively.
    8.44 +  destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
    8.45 +  tools.  Note that the latter will ignore rules declared with
    8.46 +  ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''  are used most aggressively.
    8.47    
    8.48    The classical reasoner (see \secref{sec:classical}) introduces its
    8.49    own variants of these attributes; use qualified names to access the
     9.1 --- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat Feb 28 17:08:33 2009 +0100
     9.2 +++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat Feb 28 17:09:32 2009 +0100
     9.3 @@ -3,8 +3,6 @@
     9.4  \def\isabellecontext{Quick{\isacharunderscore}Reference}%
     9.5  %
     9.6  \isadelimtheory
     9.7 -\isanewline
     9.8 -\isanewline
     9.9  %
    9.10  \endisadelimtheory
    9.11  %
    10.1 --- a/doc-src/IsarRef/Thy/document/Symbols.tex	Sat Feb 28 17:08:33 2009 +0100
    10.2 +++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Sat Feb 28 17:09:32 2009 +0100
    10.3 @@ -3,8 +3,6 @@
    10.4  \def\isabellecontext{Symbols}%
    10.5  %
    10.6  \isadelimtheory
    10.7 -\isanewline
    10.8 -\isanewline
    10.9  %
   10.10  \endisadelimtheory
   10.11  %
    11.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Sat Feb 28 17:08:33 2009 +0100
    11.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Sat Feb 28 17:09:32 2009 +0100
    11.3 @@ -3,8 +3,6 @@
    11.4  \def\isabellecontext{ZF{\isacharunderscore}Specific}%
    11.5  %
    11.6  \isadelimtheory
    11.7 -\isanewline
    11.8 -\isanewline
    11.9  %
   11.10  \endisadelimtheory
   11.11  %