Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Polynomial Theories

view this post on Zulip Email Gateway (Aug 19 2022 at 08:44):

From: Clemens Ballarin <ballarin@in.tum.de>
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).

Clemens

Last updated: Oct 31 2025 at 01:43 UTC