[isabelle-dev] FinFun syntax

[Tobias Nipkow]

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.