[isabelle] Polynomial Theories

Rene drew my attention to the fact that we currently have three theories of univariate polynomials in Isabelle:

1) HOL/Algebra/poly/Polynomial.thy
2) HOL/Algebra/UnivPoly.thy
3) HOL/Library/Polynomial.thy

There is only really a need for two: one where the carrier is a type, and one where the carrier is a set. This means that we either need 1) or 3) but not both. It looks like 3) is a modernised version of 1) (Brian, I would appreciate if you could comment on this).

If there are no strong votes against that, I will consider removing HOL/Algebra/poly/* along with HOL/Algebra/abstract/* (or submit it to the AFP).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.