It seems there is clearly a need for something of the sort to go into 
HOL/Library. Maybe it could be completely independent of Poly_Mapping, and the 
latter perhaps could be rewritten in terms of it.

Now who is volunteering to do this? I could certainly rewrite my "Frag.thy" to 
use the material I sent out yesterday and make independent of Poly_Mapping, but 
would that meet everyone's needs?


> On 25 Sep 2018, at 06:18, Akihisa Yamada <> 
> wrote:
> Dear Alexander, Florian, Larry, Manuel,
> recently I also made the same typedef, so that derivatives can be defined, 
> which wants real norm in current Isabelle/HOL. Unfortunately I didn't notice 
> it is called "poly_mapping".
> I propose calling them finsupp or finite_supp. Support is often written 
> "supp", and the term in this meaning is clearly about functions so I don't 
> think "_fun" is needed.
> Best regards,
> Akihisa

isabelle-dev mailing list

Reply via email to