I'm sure this is very useful, but I have to say once again that "Poly_Mapping" is probably not a good name for this now that it is disconnected from its original application of multivariate polynomials. I vaguely recall that we had this discussion already a while ago and didn't really resolve it.
I currently don't have any input beyond that (I'm feeling a bit poorly); I just wanted to point this out. Manuel On 03/04/2019 12:57, Lawrence Paulson wrote: > I have adopted the theory Poly_Mapping, which is part of the AFP entry > Polynomials, as the basis for a theory of finite abelian groups, which plays > a huge role in the homology development. (It concerns "almost everywhere zero > functions”.) I am gradually installing the components of this development in > various places, and think that Poly_Mapping could go into Library, as it > depends only on other Library entries. I hope nobody objects to this. Then I > guess the duplicate in the AFP should be deleted. > > I also managed to accomplish the following: > > instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector > > But I never found a use for it and I’m not sure what to do with it. > > Larry > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
