Am 12/05/2012 16:13, schrieb 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)?
JinjaThreads uses both theories. Tobias > Larry > > > > This body part will be downloaded on demand. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
