original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);

tuned names;

misc cleanup and minor performance tuning;

clarified signature;

tuned: prefer existing operations;

tuned source structure;

tuned state operations;

tuned signature;

misc tuning and clarification: prefer state operations, avoid redundant ctyp_of/cterm_of;

tuned;