invert semantics of "relevance_convergence", to make it more intuitive

if no facts were selected on first iteration, try again with a lower threshold

weed out junk in relevance filter

no need for "eq" facts -- good old "=" is good enough for us

revert unintended change

destroy elim rules before checking for finite exhaustive facts

prevent double inclusion of the fact "True_or_False" in TPTP problems

merged

tuned

merged

dropped pre_post_conv

use conv alias

preliminary versions of static_eval_conv(_simple)

use Code_Thingol.static_eval_conv_simple

added static_eval_conv

refined and unified naming convention for dynamic code evaluation techniques

tap_thy conversional

dropped now obsolete purge_data -- happens implicitly on change of theory identity

merged

introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets

added support for xsymbol syntax for mode annotations in code_pred command

tuned raw Sidekick output;

Text.Range.is_singleton;

Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;

tuned;

Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree; tuned;

tuned root markup;

misc tuning of important special cases;

Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.

merged