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