NEWS

 process, without requiring old-fashioned command-line invocation of
 "isabelle jedit -m MODE".
 
 
 *** Pure ***
+
+* Attributes "where" and "of" allow an optional context of local
+variables ('for' declaration): these variables become schematic in the
+instantiated theorem.
+
+* Obsolete attribute "standard" has been discontinued (legacy since
+Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
+where instantiations with schematic variables are intended (for
+declaration commands like 'lemmas' or attributes like "of").  The
+following temporary definition may help to port old applications:
+
+  attribute_setup standard =
+    "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
 
 * More thorough check of proof context for goal statements and
 attributed fact expressions (concerning background theory, declared
 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
 context discipline.  See also Assumption.add_assumes and the more

 (only makes sense in practice, if outer syntax is delimited
 differently).
 
 
 *** HOL ***
+
+* Simproc "finite_Collect" is no longer enabled by default, due to
+spurious crashes and other surprises.  Potential INCOMPATIBILITY.
 
 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
   "primrec_new", "primcorec", and "primcorecursive" command are now part of
   "Main".

     explicit set-comprehensions with eucl_less for other (half-) open
     intervals.
 
 
 *** ML ***
+
+* 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.
 
 * Toplevel function "use" refers to raw ML bootstrap environment,
 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
 Note that 'ML_file' is the canonical command to load ML files into the
 formal context.