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;

separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;

removed unused file;

less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;

removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping; (NB: in principle symbol abbreviations could well be ambigous);

simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output

merged

adjusted import to changed HOL theory graph

moved theory Divides after theory Nat_Numeral; tuned some proof texts

proper nested quotes; give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);