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) n
I agree in principle, but putting up a hierarchy of algebraic structures
within the constraints of Isabelle's type class system is tricky.
Additionally, sometimes adjustments have to be made since some things
that are natural in ‘regular’ mathematics are awkward to express in a
theorem prover.
*** System ***
* The Isabelle system environment always ensures that the main
executables are found within the shell search $PATH: "isabelle" and
"isabelle_scala_script".
* The Isabelle ML process is now managed directly by Isabelle/Scala, and
shell scripts merely provide optional command-line a
