1.1 --- a/doc-src/IsarRef/generic.tex	Sat Oct 15 00:08:12 2005 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Oct 15 00:08:13 2005 +0200
     1.3 @@ -375,9 +375,10 @@
     1.4  
     1.5  \subsection{Generalized elimination}\label{sec:obtain}
     1.6  
     1.7 -\indexisarcmd{obtain}
     1.8 +\indexisarcmd{obtain}\indexisarcmd{guess}
     1.9  \begin{matharray}{rcl}
    1.10    \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
    1.11 +  \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\
    1.12  \end{matharray}
    1.13  
    1.14  Generalized elimination means that additional elements with certain properties
    1.15 @@ -392,6 +393,8 @@
    1.16  \begin{rail}
    1.17    'obtain' (vars + 'and') 'where' (props + 'and')
    1.18    ;
    1.19 +  'guess' (vars + 'and')
    1.20 +  ;
    1.21  \end{rail}
    1.22  
    1.23  $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
    1.24 @@ -415,16 +418,31 @@
    1.25  Accordingly, the ``$that$'' reduction above is declared as simplification and
    1.26  introduction rule.
    1.27  
    1.28 -\medskip
    1.29 -
    1.30  In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
    1.31  meta-logical existential quantifiers and conjunctions.  This concept has a
    1.32  broad range of useful applications, ranging from plain elimination (or
    1.33 -introduction) of object-level existentials and conjunctions, to elimination
    1.34 +introduction) of object-level existential and conjunctions, to elimination
    1.35  over results of symbolic evaluation of recursive definitions, for example.
    1.36  Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
    1.37  where the result is treated as a genuine assumption.
    1.38  
    1.39 +\medskip
    1.40 +
    1.41 +The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but
    1.42 +derives the obtained statement from the course of reasoning!  The proof starts
    1.43 +with a fixed goal $thesis$.  The subsequent proof may refine this to anything
    1.44 +of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce
    1.45 +new subgoals.  The final goal state is then used as reduction rule for the
    1.46 +obtain scheme described above.  Obtained parameters $\vec x$ are marked as
    1.47 +internal by default, which prevents the proof context from being polluted by
    1.48 +ad-hoc variables.  The variable names and type constraints given as arguments
    1.49 +for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly
    1.50 +in the text.
    1.51 +
    1.52 +It is important to note that the facts introduced by $\OBTAINNAME$ and
    1.53 +$\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring
    1.54 +here are fixed in the present context!
    1.55 +
    1.56  
    1.57  \subsection{Calculational reasoning}\label{sec:calculation}
    1.58