[isabelle-dev] FinFun syntax

[Lawrence Paulson]

I'm glad we are going to move the theory into the repository. However, I would like to discuss the issue of its syntax. The presence of the letter “f" in the apply and update notation is fatal to readability:

lemma finfun_update_twist: ?a \<noteq> ?a' \<Longrightarrow> ?f(\<^sup>f ?a := ?b)(\<^sup>f ?a' := ?b') = ?f(\<^sup>f ?a' := ?b')(\<^sup>f ?a := ?b)




I also have no idea how to type these superscripts. (But it's clear that it will be tiresome.) Is there any way to overload the syntax with that used for maps, say (people are unlikely to use both notions of function in a single development)?

Larry

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120512/6282aeb3/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: finfun.png
Type: image/png
Size: 12933 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120512/6282aeb3/attachment-0002.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: finfun2.png
Type: image/png
Size: 12895 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120512/6282aeb3/attachment-0003.png>