--- /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.