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.haftm...@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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to