[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

Makarius makarius at sketis.net
Sat Sep 2 16:28:09 CEST 2017

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


More information about the isabelle-dev mailing list