use preferences.ML: do setmp *here*, to capture intended default values;

tuned;

modified proofs so that they are not using claset()

tuned lemma; replaced !! by arbitrary

Improved comment.

Documented function package in IsarRef-manual.

added variations on infinite descent

fixed Rat.inv

fixed Rat.inv

fix sgn_div_norm class

made theorem-references safe

removed unused join_mode; standard_typ_check: proper prepare_patternT, which rejects schematic type vars in non-patterns;

read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;

removed obsolete ML bindings;

linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;

mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings;

removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;

added singleton check_typ/term/prop;

removed obsolete read/cert variations (cf. Syntax.read/check);

replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

*** empty log message ***

final(?) iteration of sgn saga.

reject_vars: accept type-inference params; standard_term_check: include prepare_pattern; infer_type: mode_schematic; tuned;

exported is_param;

legacy_infer_term: ProofContext.mode_schematic;

prove: setmp quick_and_dirty (avoids race condition);

export various inner syntax modes; Syntax.add_term_check: include expand_abbrevs (consts and var bindings);

type_infer: mode_pattern;