Re: [isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

2017-09-02 Thread 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

2017-08-31 Thread Florian Haftmann 
> Is it intentional that the "Computational_Algebra" theory does not
> import "Polynomial_Factorial"?

Yes.  Polynomial_Factorial requires Field_as_Ring, which does a
substantial modification to the type class hierarchy, pulling it apart
from long-established traditions in HOL-Main.  I have been reluctant to
enforce this on any material derived from the session entry point.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

2017-08-29 Thread Manuel Eberl 
Is it intentional that the "Computational_Algebra" theory does not
import "Polynomial_Factorial"?

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev