changeset 55152 a56099a6447a
parent 55143 04448228381d
child 55183 17ec4a29ef71
--- 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