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
