1.1 --- a/src/Tools/isac/calcelems.sml	Mon Mar 19 09:48:03 2012 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Tue Mar 20 15:32:17 2012 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4     they are partially held in association lists as ref's for
     1.5     switching language levels (meta-string, object-values).
     1.6     in order to keep these ref's during re-evaluation of code,
     1.7 -   they are defined here the beginning of the code.
     1.8 -   author: Walther Neuper
     1.9 -   (c) isac-team 2003
    1.10 +   they are defined here at the beginning of the code.
    1.11 +   Author: Walther Neuper 2003
    1.12 +   (c) copyright due to lincense terms
    1.13  *)
    1.14  
    1.15  (*
    1.16 @@ -16,10 +16,14 @@
    1.17  
    1.18  type cterm' = string;
    1.19  val empty_cterm' = "empty_cterm'";
    1.20 -type thmID = string;
    1.21 +
    1.22 +type thmID = string;    (* identifier for a thm (the shortest possible identifier)       *)
    1.23 +type thmDeriv = string; (* thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name *)
    1.24 +
    1.25  type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
    1.26  type thm'' = thmID * term;
    1.27  type rls' = string;
    1.28 +
    1.29  (*.a 'guh'='globally unique handle' is a string unique for each element
    1.30     of isac's KEStore and persistent over time
    1.31     (in particular under shifts within the respective hierarchy);