2007-08-20 ago tuned CRITICAL sections;
2007-08-08 ago thread-safeness: when creating certified items, perform Theory.check_thy *last*;
2007-08-03 ago improved check_thy: produce a checked theory_ref (thread-safe version);
2007-07-23 ago marked some CRITICAL sections;
2007-07-05 ago the_theory/proof: error instead of exception Fail;
2007-06-13 ago merge/merge_refs: plain error instead of exception TERM;
2007-05-07 ago simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-04-30 ago removed obsolete get_sg;
2007-04-05 ago added thy_ord -- order of creation;
2007-04-04 ago theory: maintain ancestors in order of creation;
2007-01-21 ago tuned comments
2007-01-20 ago added is_finished_thy;
2007-01-19 ago moved ML context stuff to from Context to ML_Context;
2007-01-19 ago ML context: full generic context, tuned signature;
2006-12-30 ago removed conditional combinator;
2006-12-05 ago added mapping_result;
2006-11-24 ago fake predeclaration of structure ProofContext;
2006-10-09 ago moved Context.ml_output to Output.ml_output;
2006-10-01 ago exists_name: include this theory name;
2006-08-02 ago fake predeclaration of type Proof.context;
2006-06-07 ago fixed typo
2006-05-17 ago added mapping;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-12 ago structure Datatab: private copy avoids potential conflict of table exceptions;
2006-02-06 ago TableFun: renamed xxx_multi to xxx_list;
2006-01-21 ago rename map_theory/proof to theory/proof_map;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-13 ago added map_theory, map_proof;
2006-01-10 ago support for generic contexts with data;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago replaced DATA_FAIL by EXCEPTION;
2005-09-01 ago curried_lookup/update;
2005-08-16 ago type proof: theory_ref instead of theory (make proof contexts independent entities);
2005-07-19 ago Inttab.defined;
2005-07-06 ago check_thy: less invocations, less verbose;
2005-06-29 ago added joinable;
2005-06-22 ago begin_thy: merge maximal imports;
2005-06-20 ago improved treatment of intermediate checkpoints: actual copy
2005-06-17 ago added type theory: generic theory contexts with unique identity,
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-20 ago use_output: Symbol.escape;
2001-10-17 ago tuned comments;
2001-01-16 ago use_output: proper handling of non-ASCII symbols;
2001-01-16 ago use_text etc.: proper output of error messages;
2001-01-12 ago use_mltext: priority output;
2000-08-14 ago use_let: exclude 'val';
2000-05-05 ago tuned msg;
2000-03-06 ago added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
1999-03-09 ago tuned;
1999-02-08 ago added fetch, fetch_theory;
1999-02-05 ago setmp: theory option;
1999-02-03 ago Global theory context (used to be in Thy/context.ML);