Okay, I have replaced it by Complex_Main. In fact derivatives are only needed
in a couple of places.
Larry
> On 28 Jun 2018, at 17:03, Florian Haftmann
> wrote:
>
>> Is it right for this theory to base itself on HOL.Deriv rather than
>> Complex_Main?
>>
>> Larry
>>
>> section ‹Polynomials
> Is it right for this theory to base itself on HOL.Deriv rather than
> Complex_Main?
>
> Larry
>
> section ‹Polynomials as type over a ring structure›
>
> theory Polynomial
> imports
> HOL.Deriv
> "HOL-Library.More_List"
> "HOL-Library.Infinite_Set"
> Factorial_Ring
> begin
I don't
Is it right for this theory to base itself on HOL.Deriv rather than
Complex_Main?
Larry
section ‹Polynomials as type over a ring structure›
theory Polynomial
imports
HOL.Deriv
"HOL-Library.More_List"
"HOL-Library.Infinite_Set"
Factorial_Ring
begin