src/HOL/Import/proof_kernel.ML
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-15 wenzelm 2009-10-15 space_implode;
2009-10-15 wenzelm 2009-10-15 sort_strings (cf. Pure/library.ML);
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated ctyp/cterm operations;
2009-07-24 wenzelm 2009-07-24 ML_Context.the_local_context;
2009-07-24 wenzelm 2009-07-24 explicit OldGoals;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-11 haftmann 2009-03-11 stripped dead code
2009-03-07 wenzelm 2009-03-07 minimal adaptions for abstract binding type;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-01 wenzelm 2009-01-01 eliminated OldTerm.(add_)term_consts; eliminated polymorphic version of insert;
2008-12-31 wenzelm 2008-12-31 eliminated OldTerm.add_term_free_names;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-23 wenzelm 2008-10-23 Thm.def_name;
2008-10-22 haftmann 2008-10-22 tuned typedef interface
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-11 wenzelm 2007-10-11 moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-04-15 wenzelm 2007-04-15 removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-06 haftmann 2006-09-06 TypedefPackage.add_typedef_* now yields name of introduced type constructor
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.frees/vars_of etc.;
2006-07-04 wenzelm 2006-07-04 Thm.varifyT;
2006-06-13 wenzelm 2006-06-13 use Drule.unvarify instead of obsolete Drule.freeze_all;
2006-05-20 wenzelm 2006-05-20 List.partition;
2006-04-06 haftmann 2006-04-06 cleanup in typedef/datatype package
2006-03-14 wenzelm 2006-03-14 string_of_mixfix;
2006-02-16 obua 2006-02-16 cache improvements
2006-02-16 obua 2006-02-16 variable counter is now also cached
2006-02-16 obua 2006-02-16 adapted to kernel changes
2006-02-15 obua 2006-02-15 fixed bugs, added caching
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-22 paulson 2005-12-22 Fixed a use of an outdated Substring function
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 wenzelm 2005-10-19 replaced commafy by existing commas; avoid obsolete Goals.prin;