[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

[Makarius]

On 29/08/17 15:16, Manuel Eberl wrote:
> Is it intentional that the "Computational_Algebra" theory does not
> import "Polynomial_Factorial"?

I guess so. A comment in ROOT says (*conflicting type class
instantiations and dependent applications*), see
http://isabelle.in.tum.de/repos/isabelle/annotate/fc41a5650fb1/src/HOL/ROOT#l75


	Makarius