2005-03-24 ago Further work on interpretation commands. New command `interpret' for
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-22 ago tuned certify_typ/term;
2004-06-21 ago tuned certify_term;
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-20 ago avoid premature evaluation of syn_of (wastes time in conjunction with pp);
2004-06-09 ago added is_logtype (replaces logtypes field of syntax); tuned merge;
2004-06-01 ago proper treatment of logical types within syntax;
2004-05-29 ago improved output; refer to Pretty.pp;
2004-05-21 ago xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
2004-05-03 ago reimplementation of HOL records; only one type is created for
2004-04-29 ago warning: non-identifier declaration;
2004-04-22 ago support for advanced translation functions;
2004-02-11 ago Printing functions now use cond_extrn instead of extrn
2002-01-16 ago GPLed;
2001-12-21 ago hide: flag for full/base name;
2001-11-28 ago Syntax.read_typ: pass intern sort fn;
2001-11-28 ago data: removed obsolete finish method;
2001-11-26 ago clarified order of merge_lists';
2001-11-24 ago merge_stamps: merge_lists' with reversed args;
2001-11-09 ago theory data: finish method;
2001-11-06 ago added pretty_term', read_typ', read_typ_no_norm', read_def_terms'
2001-10-11 ago added certify_tyname;
2001-08-15 ago support for absolute namespace entry paths;
2001-01-18 ago added exists_stamp;
2000-11-10 ago added certify_tycon, certify_tyabbr, certify_const;
2000-11-06 ago added typ_instance;
2000-08-03 ago typ_no_norm;
2000-06-03 ago fixed Thm.eq_thm: use Sign.joinable;
2000-05-23 ago eta-expanded to handle value polymorphism
2000-05-21 ago removed is_type_abbr;
2000-05-05 ago added simple_read_term;
2000-04-17 ago made SML/NJ happy;
2000-04-17 ago name space hide operations;
2000-04-14 ago added is_type_abbr;
2000-03-30 ago read_def_terms (no certify yet);
2000-02-24 ago nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
1999-09-29 ago added witness_sorts, univ_witness;
1999-07-23 ago Type.norm_term;
1999-07-10 ago err_method: pass exn;
1999-06-28 ago added cond_extern_table;
1999-04-30 ago theory data: copy;
1999-03-09 ago token translation: real;
1999-02-03 ago renamed sig to PRIVATE_SIGN;
1998-12-28 ago comments
1998-10-13 ago PRIVATE sig parts;
1998-10-09 ago Unified treatment of type error msgs.
1998-10-09 ago Added a few breaks in error text.
1998-07-22 ago moved long_names / cond_extern to name_space.ML;
1998-06-05 ago improved data: secure version using Object.T and Object.kind;
1998-05-25 ago certify_term: type_check replaces Term.type_of, providing sensible
1998-05-20 ago added is_stale;
1998-05-10 ago tuned comment;
1998-05-04 ago tuned msg;
1998-04-29 ago added defaultS: sg -> sort;
1998-02-12 ago Sign.merge vs. Sign.nontriv_merge;
1998-02-12 ago fixed add_trrules: intern root;
1998-01-14 ago added of_sort;