[isabelle-dev] Poly_Mapping

Lawrence Paulson lp15 at cam.ac.uk
Wed Apr 3 16:59:37 CEST 2019

Yes, I could do that.

I was trying to figure out what the corresponding abstract topology should be, but failed. Such a thing must exist of course.


> On 3 Apr 2019, at 15:53, Fabian Immler <immler at in.tum.de> wrote:
> Given that there are several potential applications, I guess you could add it as a separate theory (Poly_Mapping_Normed_Vector_Space?) to HOL-Analysis?

More information about the isabelle-dev mailing list