Attached is a port of the HOL Light “frag” library (free Abelian groups) built upon Poly_Mapping. It’s a mess, especially with the combination of frag and Poly_Mapping names. Some of it clearly could be added to Poly_Mapping, maybe all of it. But it needs to be rationalised.
Comments / advice? Larry
Frag.thy
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
