maintain thm_name vs. derivation_id for global facts;

clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

clarified signature;

Fixed brace matching (plus some whitespace cleanup)

merged

new material on eqiintegrable functions, etc.

clarified treatment of individual theorems; tuned messages;

tuned signature;

clarified signature;

clarified derivation_name vs. raw_derivation_name;