Re: [isabelle] Locale typedef



Dear Paulo,

> Am 05.06.2018 um 19:37 schrieb Ondřej Kunčar <kuncar at in.tum.de>:
> 2. The examples from the paper as a proof text also exist in Isabelle
> and can be found in src/HOL/Types_To_Sets/Examples.
> 3. There was a meeting of Isabelle powerusers in Spain the last year and
> as far as I know the topic how to use local typedef for HOL-Algebra was
> discussed there. Maybe some of the participants could tell us more
> about the results.
I recently added another (somewhat larger) example [1] to HOL-Types_To_Sets to the development version.
So this will most likely be part of the upcoming Isabelle2018 release.

This example can be seen as one result of the discussions we had Spain:
It uses local typedef to go from the type-based linear algebra (Modules.thy, Vector_Spaces.thy) to explicit carrier sets.

Best regards,
Fabian

[1] http://isabelle.in.tum.de/repos/isabelle/file/f1f989b656bb/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy

Attachment: smime.p7s
Description: S/MIME cryptographic signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.