| 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 |
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
