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:
map_upds 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. Tobias
Description: S/MIME Cryptographic Signature