# HG changeset patch
# User wenzelm
# Date 918149517 -3600
# Node ID e5fb98fbaa76d4aa16c5e83d64efd1a533dd9fe0
# Parent  9cc37487f99567c96e035ad2ac58657a800fe621
obsolete;

diff -r 9cc37487f995 -r e5fb98fbaa76 src/Pure/Thy/README
--- a/src/Pure/Thy/README	Thu Feb 04 18:18:19 1999 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-    ID:         $Id$
-    Directory:  Pure/Thy
-    Author:     Carsten Clasohm
-    Copyright   1994 TU Muenchen
-
-
-FIXME FIXME FIXME FIXME FIXME Warning: not quite up-to-date!
-
-
-Conventions for theory- and filenames:
-
-- Files for theory T are named T.thy and T.ML where only one of these two
-  must exist.
-- Either T.thy or T.ML must define a ML structure containing an element
-  named thy (the theory).
-
-
-Information stored about loaded theories:
-
-- name of the theory
-- absolute path of the theory's files
-- time of last modification for .thy and .ML file
-  (updated when the files are read)
-- names of all read theories that depend on the theory
-- the theory as a ML object
-- theorems
-
-
-How to rebuild the theory hierarchy:
-
-The database not only contains theories read from files but also the 
-'mother of all theories' - Pure. By retrieving this theory's child list
-(i.e. the names of all theories that are extensions of it) one can build the 
-hierarchy by recursively repeating this procedure.
-
-
-The datatype used:
-
-Information is stored in the variable loaded_thys which has type
-"thy_info Symtab.table ref", i.e. as an unbalanced binary tree with
-the theory names as keys and entries of type thy_info:
-
-datatype thy_info = ThyInfo of {path: string,
-                                children: string list,
-                                thy_time: string option,
-                                ml_time: string option,
-                                theory: theory option,
-                                thms: thm Symtab.table};
-
-path: absolute path of directory where the files where located when the theory
-      was last read
-children: names of all read theories that are descendants of this theory
-thy_time: If T.thy existed this contains information about the file which
-  looks like this: Some "-rw-r--r--  1 clasohm       232 Aug 19 11:10 ".
-  Else it is 'None'.
-ml_time: same for T.ML
-theory: ML object containing the theory. As entries in loaded_thys are created
-  before the theory has been read this may be 'None' in case of an error
-  during use_thy "T".
-thms: theorems
-
-
-An entry may look like this:
-
-   ("Fun",
-      ThyInfo
-         {path = "/disk1/usr/stud/clasohm/isabelle/HOL/./",
-            thms = ?,
-            theory = Some {Pure, HOL, Ord, Set},
-            ml_time = Some "-rw-r--r--  1 clasohm      6076 Aug 30 10:04 ",
-            children = ["Prod", "subset"],
-            thy_time =
-            Some "-rw-r--r--  1 clasohm       243 Aug 19 11:02 "})
-
-
-Notes:
-
-In general all theories contained in loaded_thys are linked with Pure.
-Though stray theories are possible they are removed from loaded_thys 
-automatically as soon as update(); is used.
-
-Cycles in the hierarchy are not allowed and it is guaranteed that
-loaded_thys doesn't contain one. On the other hand this is possible
-(with all lines representing downward arrows):
-
-     A
-    / \
-   B   C
-   |   |
-   \   D
-    \ /
-     E
-
-Isabelle first searches for theory files in the directory stored in
-thy_info's path component. But in case they have been moved meanwhile
-the variable load_path (string list ref) is used to find them.