added tracing of reconstruction data

added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms

deleted SMT translation files (to be replaced by a simplified version)

move the addition of extra facts into a separate module

normalize numerals: also rewrite Numeral0 into 0

added missing rewrite rules for natural min and max

rewrite bool case expressions as if expression

simplified normalize_rule and moved it further down in the code

merged addition of rules into one function

added simplification for distinctness of small lists

moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;

conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;

the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;

avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

raise Fail uniformly for proofterm errors, which appear to be rather low-level;

unconstrainT operations on proofs, according to krauss/schropp;

added Proofterm.get_name variants according to krauss/schropp; tuned signature;

conditional structure SingleAssignment;

merged

merged

tuned proofs and fact and class names

tuned fact collection names and some proofs

grouped local statements

tuned test problems

merged

merged

simplified proof

modernized specifications;

updated/unified some legacy warnings;