revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
field_simps: better support for negation and division, and power
add divide_simps
parametricity transfer rule for INFIMUM, SUPREMUM
tuned;
more conventional tactic programming;
tuned;
proper context for print_tac;
more standard names;
prefer regular Goal_Display.pretty_goals, without censorship of options;
generalize ln/log_powr; add log_base_powr/pow
avoid confusion about pointless cursor movement with external links;
tuned
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
more appropriate name (Lifting.invariant -> eq_onp)
abstract Domainp in relator_domain rules => more natural statement of the rule
export theorems
don't forget to init Interpretation and transfer theorems in the interpretation hook
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
setup for Transfer and Lifting from BNF; tuned thm names
simplify and fix theories thanks to 356a5efdb278