added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
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).