A Consistent Foundation for Isabelle/HOL

A Correction Patch

This page presents a correction patch from the paper A Consistent Foundation for Isabelle/HOL.

The patch is supposed to be applied to Isabelle2014.

The patch can be applied by the following command provided we are in the home directory of Isabelle2014:

bash:~/Isabelle2014> patch -p1 < correction-patch-Isabelle2014

The patch can be unapplied by the following command:

bash:~/Isabelle2014> patch -p1 -R < correction-patch-Isabelle2014

There is the Example 2 from the paper with a proof of False as an Isabelle theory.
Example 2
This example does not go through after the patch is applied. This can be tested as follows:

bash:~> path/to/Isbelle2014/isabelle build -D. False

There are couple of comments on this patch (partly only for Isabelle experts):