[isabelle-dev] NEWS: discontinued obsolete attribute "standard"

[Makarius]

On Sat, 1 Feb 2014, Makarius wrote:

> Here is one more changeset to clarify that further: 04448228381d and its NEWS 
> entry:
>
> * 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
instantiated theorem.


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.


 	Makarius