[isabelle-dev] NEWS: discontinued obsolete attribute "standard"
makarius at sketis.net
Sat Feb 1 12:36:17 CET 2014
On Sat, 1 Feb 2014, Peter Lammich wrote:
> 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 ...)
> On Fr, 2014-01-31 at 18:54 +0100, Makarius wrote:
>> 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.
Applying the short story to the above example yields this:
by (auto ... dest!: sym[of "pop A" for A] ...)
That is less text, but it requires a few extra seconds of thinking which
variables are actually meant to be arbitrary in the result.
More information about the isabelle-dev