[isabelle-dev] NEWS: discontinued obsolete attribute "standard"
makarius at sketis.net
Sat Feb 1 19:36:40 CET 2014
On Sat, 1 Feb 2014, Makarius wrote:
> Here is one more changeset to clarify that further: 04448228381d and its NEWS
> * Proper context discipline for read_instantiate and instantiate_tac:
> variables that are meant to become schematic need to be given as
> fixed, and are generalized by the explicit context of local variables.
> This corresponds to Isar attributes "where" and "of" with 'for'
> declaration. INCOMPATIBILITY, also due to potential change of indices
> of schematic variables.
Yet more NEWS from that changeset:
* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
The changeset shows all that on its own
http://isabelle.in.tum.de/repos/isabelle/rev/04448228381d, but this should
be obvious on this mailing list anyway, which is ultimately about the
ongoing flow of the repository.
More information about the isabelle-dev