[isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear Florian,

thanks for the explanation and the hint on style.

The below pattern works perfectly in our formalization.

Cheers,
René

> Am 31.08.2017 um 14:03 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 
> Note that the pattern above is avoided nowadays by an interpretation
> with mixin definitions:
> 
> locale foo = fixes f :: "nat => nat"
>  assumes ...
> begin
> 
> fun bar :: "nat => nat” where ...
> 
> end
> 
> global_interpretation foo id
>  defines com = bar
>  by standard simp