# HG changeset patch # User wenzelm # Date 887291537 -3600 # Node ID bfd40126c56e4769ad225165c4ba12d0bed0b41b # Parent 72edc2a9200f961e009ecb05bf5345215d7b5957 improved comments; diff -r 72edc2a9200f -r bfd40126c56e src/Pure/README --- a/src/Pure/README Thu Feb 12 12:37:53 1998 +0100 +++ b/src/Pure/README Thu Feb 12 14:52:17 1998 +0100 @@ -1,12 +1,20 @@ 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: +This directory contains the ML source files for Pure Isabelle, which +is the basis for all object-logics: -IsaMakefile -- compiles the files + IsaMakefile compiles the Pure system + ML-Systems/ compatibility files for various ML systems + Syntax/ the syntax module + Thy/ the theory file parser and loader -Syntax/ -- the syntax module +Isabelle programmers may want to have a look at the following generic +modules: -Thy/ -- the theory file parser and loader - -ML-Systems/ -- compatibility files for various ML systems + 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)