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;