[isabelle-dev] Poly_Mapping

[Lawrence Paulson]

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