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 > <florian.haftm...@informatik.tu-muenchen.de> 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
