[isabelle-dev] NEWS: discontinued obsolete attribute "standard"

[Peter Lammich]

So, ad-hoc massaging of a lemma is no longer possible?

E.g., I often use things like 
  by (auto ... dest!: sym[of "pop A", standard] ...)

in cases where I definitely do not want to expose the subgoal where the
"pop <bound-var> = ..." occurs into Isar.

So, if I got it right, the correct way would now be:

lemmas aux = sym[of "pop A"] for A
...
by (auto ... dest: aux ...)


or, if I do not like aux-lemmas spamming my namespace:

proof -
  {fix a note sym[of "pop A"]} note aux=this
  show ?thesis by (auto ... dest: aux ...)
qed

--
  Peter





On Fr, 2014-01-31 at 18:54 +0100, Makarius wrote:
> *** 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev