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? Larry > On 25 Sep 2018, at 06:18, Akihisa Yamada <ayam...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
