Florian, On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote: > "multiplicity" is definitely interesting [...]
> I don't see why is_prime should require an algebraic_semidom [...] > Factorial rings (also known as unique factorisation domains) usually > [...] > [...] (somewhat non-standard) normalization_semidom. My general impression is that it would be good if the algebraic hierarchy that is part of standard Isabelle/HOL could follow standard mathematical definitions and nomenclature more closely. Best, Tjark _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
