[isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Frag.thy
Type: application/octet-stream
Size: 10216 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180923/6226b626/attachment.obj>