always show timing for structured proofs

use implications rather than disjunctions to improve readability

avoid name clashes

fixed more "Trueprop" issues

removed needless sort

avoid double "Trueprop"s

use original formulas for hypotheses and conclusion to avoid mismatches

track formula roles in proofs and use that to determine whether the conjecture should be negated or not

correct parsing of E dependencies

proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction

tuned

code for while directly, not via while_option

executable true liveness analysis incl an approximating version

now that sets are executable again, no more special treatment of variable sets

handle non-unit clauses gracefully