Ideas for simp trace

• click on a symbol in the resulting term and trace back which rewrite rules where used to generate this symbol
• click on a subterm of the start term to jump to the place where it is rewritten
• which rewrite rules where used to /remove/ a assumption (often assumptions get removed which are then missing for the arith tactics)
• why is certain conditional rewrite rule not applied, look at the simp trace of its conditions
  • in addition to "certain conditional rewrite rule": rewrite rules from specific theories (or rule sets like ring_simps)
  • which rewrite rules failed to apply at a particular intermediate step (perhaps also filtered by theories)
• a option to get after a (successful) simp the set of rewrite rules that were applied, such that if I were to do (simp only: that_set), the command would get the same result. (similar to sledgehammer)
  • in the same spirit: report rules that have been added explicitly (via "add:" or "using", if this is possible to detect) but not used
• search the trace for a particular rule