On Wed, 28 Oct 2009, Jasmin Christian Blanchette wrote:
> 4. Add the path "/home/nipkow/isabelle/contrib/kodkodi-1.2.3" to the
> bottom of the file "$ISABELLE_HOME/etc/components"
BTW, the new "component" concept is explain in the Isabelle system manual
section 1.1.3. In particular, users can
Hi all,
The Nitpick counterexample generator is now [*] part of Isabelle/HOL's
repository version. You can use it in any theory that imports Main.
Gotcha: You'll need to install Kodkodi (and make sure a Java
interpreter is installed).
1. Download http://www4.in.tum.de/~blanchet/kodkodi-1.2.
* New theory SupInf of the supremum and infimum operators for sets of
reals.
* New theory Probability, which contains a development of measure
theory, eventually leading to Lebesgue integration and probability.
Larry
