Isar: where attribute supports instantiation of type vars.
authorballarin
Wed Dec 10 14:27:50 2003 +0100 (2003-12-10)
changeset 1428592ed032e83a1
parent 14284 f1abe67c448a
child 14286 0ae66ffb9784
Isar: where attribute supports instantiation of type vars.
NEWS
doc-src/IsarRef/pure.tex
     1.1 --- a/NEWS	Sun Dec 07 16:30:06 2003 +0100
     1.2 +++ b/NEWS	Wed Dec 10 14:27:50 2003 +0100
     1.3 @@ -42,9 +42,10 @@
     1.4      This is consistent with the instantiation attribute "where".
     1.5  
     1.6  * Attributes "where" and "of":
     1.7 -  Now take type variables of instantiated theorem into account when reading
     1.8 -  the instantiation string.  This fixes a bug that caused instantiated
     1.9 -  theorems to have too special types in some circumstances.
    1.10 +  - Now take type variables of instantiated theorem into account when reading
    1.11 +    the instantiation string.  This fixes a bug that caused instantiated
    1.12 +    theorems to have too special types in some circumstances.
    1.13 +  - "where" permits explicit instantiations of type variables.
    1.14  
    1.15  * Calculation commands "moreover" and "also":
    1.16    Do not reset facts ("this") any more.
     2.1 --- a/doc-src/IsarRef/pure.tex	Sun Dec 07 16:30:06 2003 +0100
     2.2 +++ b/doc-src/IsarRef/pure.tex	Wed Dec 10 14:27:50 2003 +0100
     2.3 @@ -1055,17 +1055,21 @@
     2.4    \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
     2.5    effectively skipped by including ``$\_$'' (underscore) as argument.
     2.6    
     2.7 -\item [$of~\vec t$] performs positional instantiation.  The terms $\vec t$ are
     2.8 -  substituted for any schematic variables occurring in a theorem from left to
     2.9 -  right; ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
    2.10 -  following a ``$concl\colon$'' specification refer to positions of the
    2.11 -  conclusion of a rule.
    2.12 +\item [$of~\vec t$] performs positional instantiation of term
    2.13 +  variables.  The terms $\vec t$ are substituted for any schematic
    2.14 +  variables occurring in a theorem from left to right; ``\texttt{_}''
    2.15 +  (underscore) indicates to skip a position.  Arguments following a
    2.16 +  ``$concl\colon$'' specification refer to positions of the conclusion
    2.17 +  of a rule.
    2.18    
    2.19 -\item [$where~\vec x = \vec t$] performs named instantiation of schematic
    2.20 -  variables occurring in a theorem.  Schematic variables
    2.21 -  have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The
    2.22 -  question mark may be omitted if the variable name is neither a
    2.23 -  keyword nor contains a dot.
    2.24 +\item [$where~\vec x = \vec t$] performs named instantiation of
    2.25 +  schematic type and term variables occurring in a theorem.  Schematic
    2.26 +  variables have to be specified on the left-hand side (e.g.\
    2.27 +  $?x1\!.\!3$).  The question mark may be omitted if the variable name
    2.28 +  is neither a keyword nor contains a dot.  Types are instantiated
    2.29 +  before terms, and instantiations have to be written in that order.
    2.30 +  Because type instantiations are inferred from term instantiations,
    2.31 +  explicit type instantiations are seldom necessary.
    2.32  
    2.33  \end{descr}
    2.34