Changes

Summary

1. merged
2. maintain thm_name vs. derivation_id for global facts;
3. clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;
4. clarified signature;
5. Fixed brace matching (plus some whitespace cleanup)
6. merged
7. new material on eqiintegrable functions, etc.
8. clarified treatment of individual theorems; tuned messages;
9. tuned signature;
10. clarified signature;
11. clarified derivation_name vs. raw_derivation_name;