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?


Attachment: Frag.thy
Description: Binary data

isabelle-dev mailing list

Reply via email to