src/Pure/README

new datatype theory, supports 'draft theories' and incremental extension:
add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i,
add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i,
add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname;
added merge_thy_list for multiple merges and extend-merges;
added rep_theory, subthy, eq_thy, cert_axm, read_axm;
changed type of axioms_of;
renamed internal merge_theories to merge_thm_sgs;
various internal changes of thm and theory related code;

                        Pure: The Pure Isabelle System

This directory contains the ML source files for Pure Isabelle, which is the
basis for all object-logics.  Important files include:

Makefile -- compiles the files under Poly/ML or SML of New Jersey

Syntax/  -- subdirectory containing the syntax module

Thy/     -- subdirectory containing the thy file parser and loader

ROOT.ML  -- loads all source files.  Enter ML and type:  use "ROOT.ML";

NJ.ML    -- compatibility file for Standard ML of New Jersey.  You may wish to
            alter the parameter settings.

POLY.ML  -- compatibility file for Poly/ML