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

[Makarius]

On Sat, 1 Feb 2014, Peter Lammich wrote:

>
>>    by (auto ... dest!: sym[of "pop A" for A] ...)
>>
>
> If this is now supported (it's not in 2013-2, where standard is already
> deprecated): Nice feature! I have no objections left against removing
> standard ;)

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.


These things are only relevant for really old tools, or people who have 
studied old tools at some point.  Just empirically, read_instantiate and 
instantiate_tac are so rare that it is hardly worth mentioning them, but 
I've made the text above explicit, since there will be inevitable theories 
from the 1990-ies that need to be refurbished.


 	Makarius