> 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
