added String.isSubstring;

export is_finished; added thy_ord (based on update_time); begin_thy/register_thy: more precise handling of update_time;

Present.session_name;

tuned signature; tuned message;

thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;

removed thy_ord (erratic due to multi-threading);

some cleaning up

theorem: apply hook last;

reset goal messages after goal update;

added hilite markup;

fixed type alias in signature;

added lemma

allow TVars during type inference

tidied the proofs

made smlnj happy;

new fun declaration

Auto-config of E_HOME, SPASS_HOME, VAMPIRE_HOME

Vampire structured proofs. Better parsing; some bug fixes.

chained facts are now included

new proofs found

trivial cleaning up

added goal_message;

theorem hooks: apply in declaration order;

Generalized code generator for numerals.

- New theories Lambda/NormalForm and Lambda/Standardization - Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories

Added lecture notes by Matthes and Loader.

New proof of standardization theorem (inspired by Ralph Matthes).

Definition of normal forms (taken from theory WeakNorm).

Moved definition of normal forms to new NormalForm theory.

Added Standardization theory.

New code generator setup (taken from Library/Executable_Real.thy, also works for old code generator).

Added code generator setup (taken from Library/Executable_Rat.thy, also works for old code generator).

Integrated code generator setup into RealDef theory.

Integrated code generator setup into Rational theory.

Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories.

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;