-This directory contains the Standard ML sources of the Isabelle system for
-ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files
-include
-
-
-
Makefile
-
compiles the files under Poly/ML or SML of New Jersey. Can also
-run all the tests described below.
+This directory contains the ML sources of the Isabelle system for
+ZF Set Theory, based on FOL.
-
ROOT.ML
-
loads all source files. Enter an ML image containing FOL and
-type: use "ROOT.ML";
-
-
-There are also several subdirectories of examples. To execute the examples on
-some directory <Dir>, enter an ML image containing ZF and type
-use "<Dir>/ROOT.ML";
-
+There are several subdirectories of examples:
AC
subdirectory containing proofs from the book "Equivalents of the Axiom