[isabelle-dev] Frag / Poly_Mapping
lp15 at cam.ac.uk
Sun Sep 23 20:59:42 CEST 2018
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?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 10216 bytes
Desc: not available
More information about the isabelle-dev