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;

added mk_conjunction_list;

Goal.prove: more tactic arguments;

Checking for unsound proofs. Tidying.

"all theorems" mode forces definition-expansion off. signature tidying

title fixed

replaced extern_skolem by slightly more simplistic revert_skolems; moved fix_frees to variable.ML;

renamed ProofContext.fix_frees to Variable.fix_frees;

replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;