--- a/NEWS Mon Jan 27 16:38:52 2014 +0000
+++ b/NEWS Mon Jan 27 17:13:33 2014 +0000
@@ -40,6 +40,19 @@
*** 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
@@ -53,6 +66,9 @@
*** 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
@@ -266,6 +282,13 @@
*** 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