[isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

Lawrence Paulson lp15 at cam.ac.uk
Thu Jun 28 17:53:06 CEST 2018


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



More information about the isabelle-dev mailing list