Pure: The Pure Isabelle System
This directory contains the ML source files for Pure Isabelle, which
is the basis for all object-logics:
IsaMakefile compiles the Pure system (use isatool make)
ML-Systems/ compatibility files for various ML systems
General/ general tools
Syntax/ the syntax module
Thy/ the theory file parser (old format) and loader
Isar/ Intelligible Semi-Automated Reasoning subsystem
./ the actual meta logic implementation (see ROOT.ML)
Isabelle programmers may want to have a look at the generic modules
Library (see library.ML) and those in General/ (see General/README).