tuned whitespace;

unregister: eliminated unused status;

proper header;

proper header; tuned whitespace;

proper header; adapted ResBlacklist -- eliminated inefficient hash table; eliminated some old folds;

separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

Named_Thms is not scalable;

replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space; tuned;

tuned;

tuned proof;