--- 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
--- a/src/Doc/IsarRef/Generic.thy Sun Jan 26 13:45:40 2014 +0100
+++ b/src/Doc/IsarRef/Generic.thy Sun Jan 26 14:01:19 2014 +0100
@@ -132,7 +132,6 @@
@{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
@{attribute_def rotated} & : & @{text attribute} \\
@{attribute_def (Pure) elim_format} & : & @{text attribute} \\
- @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
@{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
\end{matharray}
@@ -180,11 +179,6 @@
Note that the Classical Reasoner (\secref{sec:classical}) provides
its own version of this operation.
- \item @{attribute standard} puts a theorem into the standard form of
- object-rules at the outermost theory level. Note that this
- operation violates the local proof context (including active
- locales).
-
\item @{attribute no_vars} replaces schematic variables by free
ones; this is mainly for tuning output of pretty printed theorems.
--- a/src/Pure/Pure.thy Sun Jan 26 13:45:40 2014 +0100
+++ b/src/Pure/Pure.thy Sun Jan 26 14:01:19 2014 +0100
@@ -175,10 +175,6 @@
"Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
"named rule parameters"
-attribute_setup standard =
- "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
- "result put into standard form (legacy)"
-
attribute_setup rule_format = {*
Scan.lift (Args.mode "no_asm")
>> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)