lin_arith_prover splits certain operators (e.g. min, max, abs)

proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust

comment (timing information for last example) added

possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed

removed skip

Added in code to check too general axiom clauses.

exported attrib;

lin_arith_prover splits certain operators (e.g. min, max, abs)

fixed a bug in function poly: decomposition of products

Function package can now do automatic splits of overlapping datatype patterns

Removed an "apply arith" where there are already "No Subgoals"

code reformatted

Additional freshness constraints for FCB.

proper Element.generalize_facts;

add_consts: proper Sign.full_name; sortcontext_of_typ: avoid freeze_thaw, tuned;

added generalize_facts; tuned;

added maxidx_values;

export: refrain from adjusting maxidx;

adjust_maxidx: pass explicit lower bound; tuned interfaces;

Thm.adjust_maxidx;

removed unused add_in_order/add_once (cf. OrdList.insert);

demod_rule: depend on context, proper Variable.import/export;

tuned proofs;

lin_arith_prover splits certain operators (e.g. min, max, abs)

bugfix related to cancel_div_mod simproc

lin_arith_prover splits certain operators (e.g. min, max, abs)

rename legacy_pretty_thm to pretty_thm_legacy;

tuned comment;

added add_fixes_direct; tuned;

prove: proper assumption context, more tactic arguments; tuned;