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

[Makarius]

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.


 	Makarius