18 lines
697 B
Plaintext
18 lines
697 B
Plaintext
Isabelle is a generic proof assistant. It allows mathematical formulas
|
|
to be expressed in a formal language and provides tools for proving
|
|
those formulas in a logical calculus. Isabelle was originally
|
|
developed at the University of Cambridge and Technische Universität
|
|
München, but now includes numerous contributions from institutions and
|
|
individuals worldwide.
|
|
|
|
Isabelle is written in polyML, Java, and Scala, but does not require
|
|
them to be installed from SBo.
|
|
|
|
This build is bundling: jEdit, vscodium, jdk-17, so be careful about
|
|
its interference with other packages.
|
|
|
|
A lot of proofs certified with Isabelle can be found on
|
|
https://www.isa-afp.org/
|
|
|
|
This build repackages the binary build.
|