Re: [isabelle] Reconciling FinFuns in Distro and AFP

On 04/09/2016 21:04, Florian Haftmann wrote:
c) maybe also go for a general cleanup of Map.thy in the long run.

Yes, that would be nice. Although, when I just went through it, only the following concept seems too specilized and should be moved somewhere else:


In fact, I suspect it is only used in Jinja* in the AFP and could be moved there.

Potentially also restrict_map, although that is a natural operation. [It's math syntax would ideally use the symbol \upharpponright, but that does not exist yet.]

And map_le should be renamed to le_map.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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