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
