author | ballarin |

Wed Dec 10 14:27:50 2003 +0100 (2003-12-10) | |

changeset 14285 | 92ed032e83a1 |

parent 14284 | f1abe67c448a |

child 14286 | 0ae66ffb9784 |

Isar: where attribute supports instantiation of type vars.

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