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/annotat
Here is some timing information for standard variations on "isabelle
build -a", see details below.
The hardware is lxcisa0 at TUM, which is an Intel Xeon with many cores.
(Lars Hupel can explain the precise hardware setup).
The canonical build parameters for this machine appear to be:
isabell
