src/Pure/context.ML
2006-10-09 wenzelm 2006-10-09 moved Context.ml_output to Output.ml_output;
2006-10-01 wenzelm 2006-10-01 exists_name: include this theory name;
2006-08-02 wenzelm 2006-08-02 fake predeclaration of type Proof.context;
2006-06-07 haftmann 2006-06-07 fixed typo
2006-05-17 wenzelm 2006-05-17 added mapping;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-12 wenzelm 2006-02-12 structure Datatab: private copy avoids potential conflict of table exceptions; simplified TableFun.join;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
2006-01-21 wenzelm 2006-01-21 rename map_theory/proof to theory/proof_map; added separate map_theory/proof;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; use_output: Output.ML_errors;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 wenzelm 2006-01-13 added map_theory, map_proof;
2006-01-10 wenzelm 2006-01-10 support for generic contexts with data;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 replaced DATA_FAIL by EXCEPTION;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 type proof: theory_ref instead of theory (make proof contexts independent entities); added transfer_proof;
2005-07-19 wenzelm 2005-07-19 Inttab.defined;
2005-07-06 wenzelm 2005-07-06 check_thy: less invocations, less verbose; tuned merge, merge_refs;
2005-06-29 wenzelm 2005-06-29 added joinable;
2005-06-22 wenzelm 2005-06-22 begin_thy: merge maximal imports; incorporate proof data; added generic context;
2005-06-20 wenzelm 2005-06-20 improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;
2005-06-17 wenzelm 2005-06-17 added type theory: generic theory contexts with unique identity, arbitrarily typed data, linear and graph development -- a complete rewrite of code that used to be spread over in sign.ML, theory.ML, theory_data.ML, pure_thy.ML;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 use_output: Symbol.escape;
2001-10-17 wenzelm 2001-10-17 tuned comments;
2001-01-16 wenzelm 2001-01-16 use_output: proper handling of non-ASCII symbols;
2001-01-16 wenzelm 2001-01-16 use_text etc.: proper output of error messages;
2001-01-12 wenzelm 2001-01-12 use_mltext: priority output;
2000-08-14 wenzelm 2000-08-14 use_let: exclude 'val';
2000-05-05 wenzelm 2000-05-05 tuned msg;
2000-03-06 wenzelm 2000-03-06 added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
1999-03-09 wenzelm 1999-03-09 tuned;
1999-02-08 wenzelm 1999-02-08 added fetch, fetch_theory;
1999-02-05 wenzelm 1999-02-05 setmp: theory option; save;
1999-02-03 wenzelm 1999-02-03 Global theory context (used to be in Thy/context.ML);