discontinued obsolete attribute "standard";
authorwenzelm
Sun Jan 26 14:01:19 2014 +0100 (2014-01-26)
changeset 55152a56099a6447a
parent 55151 f331472f1027
child 55153 eedd549de3ef
discontinued obsolete attribute "standard";
NEWS
src/Doc/IsarRef/Generic.thy
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sun Jan 26 13:45:40 2014 +0100
     1.2 +++ b/NEWS	Sun Jan 26 14:01:19 2014 +0100
     1.3 @@ -44,6 +44,15 @@
     1.4  variables ('for' declaration): these variables become schematic in the
     1.5  instantiated theorem.
     1.6  
     1.7 +* Obsolete attribute "standard" has been discontinued (legacy since
     1.8 +Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
     1.9 +where instantiations with schematic variables are intended (for
    1.10 +declaration commands like 'lemmas' or attributes like "of").  The
    1.11 +following temporary definition may help to port old applications:
    1.12 +
    1.13 +  attribute_setup standard =
    1.14 +    "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
    1.15 +
    1.16  * More thorough check of proof context for goal statements and
    1.17  attributed fact expressions (concerning background theory, declared
    1.18  hyps).  Potential INCOMPATIBILITY, tools need to observe standard
     2.1 --- a/src/Doc/IsarRef/Generic.thy	Sun Jan 26 13:45:40 2014 +0100
     2.2 +++ b/src/Doc/IsarRef/Generic.thy	Sun Jan 26 14:01:19 2014 +0100
     2.3 @@ -132,7 +132,6 @@
     2.4      @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
     2.5      @{attribute_def rotated} & : & @{text attribute} \\
     2.6      @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
     2.7 -    @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
     2.8      @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
     2.9    \end{matharray}
    2.10  
    2.11 @@ -180,11 +179,6 @@
    2.12    Note that the Classical Reasoner (\secref{sec:classical}) provides
    2.13    its own version of this operation.
    2.14  
    2.15 -  \item @{attribute standard} puts a theorem into the standard form of
    2.16 -  object-rules at the outermost theory level.  Note that this
    2.17 -  operation violates the local proof context (including active
    2.18 -  locales).
    2.19 -
    2.20    \item @{attribute no_vars} replaces schematic variables by free
    2.21    ones; this is mainly for tuning output of pretty printed theorems.
    2.22  
     3.1 --- a/src/Pure/Pure.thy	Sun Jan 26 13:45:40 2014 +0100
     3.2 +++ b/src/Pure/Pure.thy	Sun Jan 26 14:01:19 2014 +0100
     3.3 @@ -175,10 +175,6 @@
     3.4    "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
     3.5    "named rule parameters"
     3.6  
     3.7 -attribute_setup standard =
     3.8 -  "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
     3.9 -  "result put into standard form (legacy)"
    3.10 -
    3.11  attribute_setup rule_format = {*
    3.12    Scan.lift (Args.mode "no_asm")
    3.13      >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)