--- a/NEWS Sun Jan 26 13:45:40 2014 +0100
+++ b/NEWS Sun Jan 26 14:01:19 2014 +0100
@@ -44,6 +44,15 @@
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