author wenzelm
Thu, 12 Feb 1998 14:52:17 +0100
changeset 4620 bfd40126c56e
parent 3279 815ef5848324
child 4689 49d116fdcafa
permissions -rw-r--r--
improved comments;

                        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
  ML-Systems/   compatibility files for various ML systems
  Syntax/     	the syntax module
  Thy/          the theory file parser and loader

Isabelle programmers may want to have a look at the following generic

  Library	basic library (see library.ML)
  TableFun	efficient tables (see table.ML)
  Seq		unbounded sequences (see seq.ML)
  Pretty	pretty printing module (see Syntax/pretty.ML)
  Scanner	scanner toolbox (see Syntax/lexicon.ML)
  Path		abstract algebra of file paths (see Thy/path.ML)
  File		file system operations (see Thy/file.ML)