Now based on Complex_Main, not HOL.Deriv
authorpaulson <lp15@cam.ac.uk>
Fri, 29 Jun 2018 14:00:37 +0100
changeset 68534 914e1bc7369a
parent 68533 7da59435126a
child 68535 4d09df93d1a2
Now based on Complex_Main, not HOL.Deriv
src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 29 11:39:40 2018 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 29 14:00:37 2018 +0100
@@ -9,7 +9,7 @@
 
 theory Polynomial
 imports
-  HOL.Deriv
+  Complex_Main
   "HOL-Library.More_List"
   "HOL-Library.Infinite_Set"
   Factorial_Ring