Public Repository

Last pushed: 2 years ago
Short Description
Isabelle theorem prover
Full Description

Isabelle: https://isabelle.in.tum.de/
Dockerfile's: https://github.com/dominique-unruh/isabelle-docker

Use the tag to chose the required Isabelle logic.

  • Pure -> pure2015
  • HOL -> hol2015
  • HOL-Multivariate_Analysis -> multivariate2015
    (The number 2015 indicates the Isabelle version.)

If additional logics should be added, please write me a message.

For easy access, use the command docker-runx (https://github.com/dominique-unruh/isabelle-docker/blob/master/docker-runx). It mounts the current directory into /home/user/data and opens an X11 connection (assuming Linux).
Example:

  • ./docker-runx unruh/isabelle:hol isabelle build -d . MyHeap
  • ./docker-runx unruh/isabelle:multivariate isabelle jedit Test.thy
Docker Pull Command
Owner
unruh