[isabelle-dev] FinFun syntax

Tobias Nipkow nipkow at in.tum.de
Sat May 12 17:11:37 CEST 2012

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.


> Larry
> This body part will be downloaded on demand.

More information about the isabelle-dev mailing list