[isabelle] Reconciling FinFuns in Distro and AFP

Hi all,

back in 2012 theory FinFun has been placed in HOL/Library and the
corresponding AFP been left Âas it isÂ.  (I remember me also being
involved into that decision).

Despite the initial enthusiasm, uses of that theory remained rare.
Taking that into account and further the increase of reuse in the AFP,
it seems time to reconcile the distro version back into the AFP.

Are there any comments on this?

This measure is part of a bigger plan to
a) introduce a type of finite mappings;
b) let Mapping.thy base on that (as far as appropriate);
c) maybe also go for a general cleanup of Map.thy in the long run.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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