*** Pure ***
* 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))"
New in Isabelle2012 (May 2012)
------------------------------
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
old-style "standard" after instantiation or composition of facts
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of
indices of schematic variables.
This refers to Isabelle/a56099a6447a.
I was unsure if that had to be explicitly announced here at all --
"standard" became out of use many years ago. There were only very few
left-over applications due to lack of "eigen-context" for instantiations.
So the short story is: Whenever an ancient "standard" pops out of the
mists of time, remove it, and potentially say "for x y z" according to
what is actually intended. Either in a narrow scope within the "of" /
"where" attribute, or in a broader scope around a 'lemmas' / 'theorems' /
'declares' command.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
