Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy
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 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 think so, especially the combination of theories from > HOL-Library with a non-canonical theory entry is weird. > > I am unable to tell on the spot how this has emerged. Are there any > suspicious things when HOL.Deriv is replaces by Complex_Main? > > I guess that theory uses some analytical results and hence cannot build > on Main alone. signature.asc Description: Message signed with OpenPGP ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy
> 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 think so, especially the combination of theories from HOL-Library with a non-canonical theory entry is weird. I am unable to tell on the spot how this has emerged. Are there any suspicious things when HOL.Deriv is replaces by Complex_Main? I guess that theory uses some analytical results and hence cannot build on Main alone. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL/Computational_Algebra/Polynomial.thy
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
