Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

2018-06-29 Thread Lawrence Paulson
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

Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

2018-06-28 Thread Florian Haftmann
> 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

[isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

2018-06-28 Thread Lawrence Paulson
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