# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530277237 -3600
# Node ID 914e1bc7369abee4bbe30a6707e406473511e0da
# Parent  7da59435126a007305f45729ce479d1a4d7e4ae0
Now based on Complex_Main, not HOL.Deriv

diff -r 7da59435126a -r 914e1bc7369a 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