export tsig_of;

clarified role of class relations

ignore mutual recursive modules

integer compatibility: added wrapper for structure Time;

fixed use_text;

downgraded IntInf with divMod; fixed use_text;

added auto-quickcheck-time-limit;

auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;

added auto_quickcheck feature;

Norbert Schirmer: record improvements;

preliminary material for Isabelle2007;

misc tuning and update;

misc tuning and update;

misc tuning and update;

updated year to 2007;

tuned;

added some lemmas

print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);

ContextPosition.put_ctxt;

NameSelection: more interval checks;

tuned message;

turned into generic context data;

ML_setup for bind_thms;

Simplified interface for printing of interpretations.

unfold_locales workaround

Theory/context data restructured; simplified interface for printing of interpretations.

fixed dir in single-logic test

llabs/sko: removed Name.internal;

avoid unnamed infixes;

avoid internal names;

switch notification email back on

fix shell quoting confusion

local_theory transactions: more careful treatment of context position;

keep context position as tags for consts/thms;

add_abbrev: tags (Markup.property list);

added internalK, property_internal;

add_consts_authentic/add_abbrev: tags (Markup.property list); tuned signature;

Markup.internalK;

print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;

added properties_of;

maintain tags (Markup.property list); tuned;

skofuns/absfuns: explicit markup as internal consts;

Sign.add_consts_authentic: tags (Markup.property list);

standard_term_check: include expand_abbrevs (back again);

added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;

removed redundant const_constraint; add_const_constraint: proper certification; prepare_dummies: avoid imperative features; term_check: separate phases, standard_infer_types passes inference parameters instead of frees/vars; Syntax.install_operations: dummy unparsers;

Sign.add_const_constraint; Syntax.add_typ/term_check: added stage and name argument;

maintain maxidx (analogous to name context); polymorhic: observe Variable.maxidx_of;

added fixate_params; type_infer: freeze_mode = NONE keeps inference parameters in result; type_infer: observe Variable.maxidx_of;

Sign.the_const_constraint;

added declare_typ_names; replace_dummy_patterns: canonical argument order;

removed obsolete external interface add_const_constraint; removed redundant const_constraint; renamed add_const_constraint_i to add_const_constraint;

Sign.add_const_constraint;

fixed metis proof (Why did it stop working?);

swapped machines for at-sml-dev and at-sml-dev-p

no proof terms for smlnj

add -p 2 at-sml-dev test for HOL proof terms sessions only

at-sml-dev session with -p 2

Added target for proof term sessions (those that need -p 2)

accept single logic and target as argument