[isabelle-dev] Frag / Poly_Mapping

Lawrence Paulson lp15 at cam.ac.uk
Tue Sep 25 16:33:51 CEST 2018

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 <ayamada at trs.cm.is.nagoya-u.ac.jp> 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

More information about the isabelle-dev mailing list