src/Pure/sign.ML
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-16 wenzelm 2005-04-16 added del_modesyntax(_i); added print_all_data;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** added declared_tyname/const and read_tyname/const; removed certify_tyname/const; added prep_ext_merge, nontriv_merge kept internal; efficient subsig test;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-22 wenzelm 2004-06-22 tuned certify_typ/term;
2004-06-21 wenzelm 2004-06-21 tuned certify_term;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-20 wenzelm 2004-06-20 avoid premature evaluation of syn_of (wastes time in conjunction with pp);
2004-06-09 wenzelm 2004-06-09 added is_logtype (replaces logtypes field of syntax); tuned merge;
2004-06-01 wenzelm 2004-06-01 proper treatment of logical types within syntax;
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
2004-05-03 schirmer 2004-05-03 reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
2004-04-29 wenzelm 2004-04-29 warning: non-identifier declaration;
2004-04-22 wenzelm 2004-04-22 support for advanced translation functions;
2004-02-11 berghofe 2004-02-11 Printing functions now use cond_extrn instead of extrn (due to short_names flag)
2002-01-16 wenzelm 2002-01-16 GPLed;
2001-12-21 wenzelm 2001-12-21 hide: flag for full/base name;
2001-11-28 wenzelm 2001-11-28 Syntax.read_typ: pass intern sort fn;
2001-11-28 wenzelm 2001-11-28 data: removed obsolete finish method;
2001-11-26 wenzelm 2001-11-26 clarified order of merge_lists';
2001-11-24 wenzelm 2001-11-24 merge_stamps: merge_lists' with reversed args;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-11-06 wenzelm 2001-11-06 added pretty_term', read_typ', read_typ_no_norm', read_def_terms' which refer to local syntax;
2001-10-11 wenzelm 2001-10-11 added certify_tyname;
2001-08-15 wenzelm 2001-08-15 support for absolute namespace entry paths;
2001-01-18 wenzelm 2001-01-18 added exists_stamp; added PureN, CPureN;
2000-11-10 wenzelm 2000-11-10 added certify_tycon, certify_tyabbr, certify_const;
2000-11-06 wenzelm 2000-11-06 added typ_instance;
2000-08-03 wenzelm 2000-08-03 typ_no_norm;
2000-06-03 wenzelm 2000-06-03 fixed Thm.eq_thm: use Sign.joinable;
2000-05-23 paulson 2000-05-23 eta-expanded to handle value polymorphism
2000-05-21 wenzelm 2000-05-21 removed is_type_abbr; added certify_class, certify_sort, read_sort; adapted to inner syntax of sorts;
2000-05-05 wenzelm 2000-05-05 added simple_read_term;
2000-04-17 wenzelm 2000-04-17 made SML/NJ happy;
2000-04-17 wenzelm 2000-04-17 name space hide operations;
2000-04-14 wenzelm 2000-04-14 added is_type_abbr;
2000-03-30 wenzelm 2000-03-30 read_def_terms (no certify yet);
2000-02-24 wenzelm 2000-02-24 nodup_vars: fixed omission of 2 minor cases; account for Frees as well;
1999-09-29 wenzelm 1999-09-29 added witness_sorts, univ_witness; removed nonempty_sort;
1999-07-23 wenzelm 1999-07-23 Type.norm_term;
1999-07-10 wenzelm 1999-07-10 err_method: pass exn; nontriv_merge: no handle_error;
1999-06-28 wenzelm 1999-06-28 added cond_extern_table;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-03-09 wenzelm 1999-03-09 token translation: real;
1999-02-03 wenzelm 1999-02-03 renamed sig to PRIVATE_SIGN;
1998-12-28 paulson 1998-12-28 comments
1998-10-13 wenzelm 1998-10-13 PRIVATE sig parts;
1998-10-09 nipkow 1998-10-09 Unified treatment of type error msgs.
1998-10-09 nipkow 1998-10-09 Added a few breaks in error text.
1998-07-22 wenzelm 1998-07-22 moved long_names / cond_extern to name_space.ML;
1998-06-05 wenzelm 1998-06-05 improved data: secure version using Object.T and Object.kind;
1998-05-25 wenzelm 1998-05-25 certify_term: type_check replaces Term.type_of, providing sensible error messages; eliminated mapfilt_atoms (use Term.foldl_aterms);
1998-05-20 wenzelm 1998-05-20 added is_stale;
1998-05-10 wenzelm 1998-05-10 tuned comment;
1998-05-04 wenzelm 1998-05-04 tuned msg;