Re: [isabelle] finite sets and code generation, once again



Hi Peter,

> What's about
>     d) Parameterize over choice-function (e.g. using a locale, fixing
> choice and assuming: "s~={} ==> choice s : s"), do your definition
> inside this locale
>         and then instantiate to concrete set implementation ?

yes, that is also a possibility.  (I had the already the strong
impression that I missed something).

Thanks for pointing this out.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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