diff -r 5a6b0ed377cb -r 9154d8410514 src/Pure/Thy/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/README	Thu Sep 08 13:17:57 1994 +0200
@@ -0,0 +1,93 @@
+    ID:         $Id$
+    Directory:  Pure/Thy
+    Author:     Carsten Clasohm
+    Copyright   1994 TU Muenchen
+
+
+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.