2007-08-27 ago added simple definition scheme
2007-08-13 ago moved appl syntax to PureThy;
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-28 ago removed dead code;
2007-07-23 ago marked some CRITICAL sections;
2007-07-08 ago thm tag: list;
2007-05-07 ago simplified DataFun interfaces;
2007-04-26 ago renamed some old names to;
2007-02-26 ago Thm.internalK;
2007-02-26 ago removed obsolete theorem_space;
2007-02-06 ago added has_kind/get_kind;
2007-02-01 ago proper use of PureThy.has_name_hint instead of hard-wired string'';
2007-01-31 ago Expose hard-wired string which was changed and broke Proof General.
2007-01-19 ago moved thm/thms to ml_context.ML;
2007-01-19 ago adapted ML context operations;
2006-12-30 ago added has_name_hint;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-11-30 ago Theory.merge_list;
2006-11-29 ago *** bad commit -- reverted to previous version ***
2006-11-29 ago added map/burrow_facts;
2006-11-29 ago added map/burrow_facts;
2006-11-28 ago added burrow_fact;
2006-11-26 ago updated (binder) syntax/notation;
2006-11-23 ago tuned;
2006-11-21 ago moved theorem kinds from PureThy to Thm;
2006-10-04 ago *** empty log message ***
2006-09-21 ago member (op =);
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-08 ago tuned exception handling;
2006-06-05 ago support embedded terms;
2006-05-13 ago added add_defs_unchecked(_i);
2006-05-05 ago added syntax for _type_constraint_;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-04-13 ago moved print_theorems/theory to Isar/proof_display.ML;
2006-04-10 ago Term.itselfT;
2006-03-21 ago avoid polymorphic equality;
2006-02-22 ago simplified Pure conjunction, based on actual const;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-01-29 ago proper order of trfuns;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-25 ago export name_multi;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-13 ago generic_setup: optional argument, defaults to Context.setup();
2006-01-07 ago gen_names: preserve empty names;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-12-06 ago re-oriented some result tuples in PureThy
2005-10-28 ago datatype thmref: added Fact;
2005-10-19 ago added thm(s) retrieval functions (from goals.ML);
2005-09-29 ago Theory.add_finals_i;
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago added generic_setup, add_oracle (from isar_thy.ML);
2005-09-01 ago curried_lookup/update;
2005-08-28 ago export theorems_of;
2005-08-01 ago Compress.init_data;
2005-07-13 ago (intermediate commit)