src/Pure/sign.ML
1998-02-12 wenzelm 1998-02-12 Sign.merge vs. Sign.nontriv_merge;
1998-02-12 wenzelm 1998-02-12 fixed add_trrules: intern root;
1998-01-14 wenzelm 1998-01-14 added of_sort;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP;
1997-12-02 wenzelm 1997-12-02 tuned trfuns types;
1997-11-20 wenzelm 1997-11-20 improved error msg;
1997-11-20 wenzelm 1997-11-20 removed data.ML (made part of sign.ML);
1997-11-20 wenzelm 1997-11-20 exported pretty_classrel, pretty_arity; added infer_types_simult; tuned infer_types interface; moved print_sg to display.ML;
1997-11-14 wenzelm 1997-11-14 merge_refs: check for different versions of theories;
1997-11-13 wenzelm 1997-11-13 export read_raw_typ;
1997-11-05 wenzelm 1997-11-05 adapted add_trfunsT;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-10-31 wenzelm 1997-10-31 *** empty log message ***
1997-10-31 wenzelm 1997-10-31 added str_of_sg: sg -> string; improved error handling of data access;
1997-10-28 wenzelm 1997-10-28 add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons, add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;
1997-10-27 wenzelm 1997-10-27 made SML/NJ happy;
1997-10-24 wenzelm 1997-10-24 self_ref: check_stale; moved pure stuff to pure_thy.ML;
1997-10-23 wenzelm 1997-10-23 hide id, stamps; added stamp_names_of, name_of; replaced make_draft by prep_ext; improved print_sg; tuned;
1997-10-22 wenzelm 1997-10-22 certify: check_stale;
1997-10-21 wenzelm 1997-10-21 sg_ref: automatic adjustment of thms of draft theories;
1997-10-20 wenzelm 1997-10-20 tuned types;
1997-10-20 wenzelm 1997-10-20 fixed types of add_XXX; added base_name; tuned exports; tuned output of sg;
1997-10-16 wenzelm 1997-10-16 fixed prep_ext;
1997-10-16 wenzelm 1997-10-16 improved pretty_arity;
1997-10-15 wenzelm 1997-10-15 make_draft replaced by prep_ext; improved print_data; merge now does trivial (absorptive) merges only; added nontriv_merge;
1997-10-14 wenzelm 1997-10-14 added additional generic data;
1997-10-13 wenzelm 1997-10-13 fixed extern; added str_of_classrel, str_of_arity, str_of_arity;
1997-10-13 wenzelm 1997-10-13 merge: drops path elements;
1997-10-09 wenzelm 1997-10-09 tuned exports; tuned add_space; tuned print_sg; fixed "op ==>" syntax;
1997-10-07 wenzelm 1997-10-07 improved types of add_XXX funs (xtyp etc.); tuned comments; tuned msgs; improved merge: no longer raises ERROR, but TERM;
1997-10-06 wenzelm 1997-10-06 now supports qualified names (intern vs. extern) !!! added long_names: bool ref (initially false); new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i; rep_sg: added path, spaces; added pretty_sort (uses proper syntax); improved print_sg; eliminated raise_term, raise_typ;
1997-07-22 wenzelm 1997-07-22 tuned error / warning;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-16 wenzelm 1997-04-16 renamed subclass to classrel; tune type checking error msgs;
1997-02-28 wenzelm 1997-02-28 added add_tokentrfuns;
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1997-02-06 wenzelm 1997-02-06 adapted to new Syntax.read_typ;
1996-12-13 wenzelm 1996-12-13 added typed print translations;
1996-12-10 wenzelm 1996-12-10 add_modesyntax(_i): added 'inout' argument;
1996-11-27 wenzelm 1996-11-27 renamed "symbolfont" to "symbols";
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-19 wenzelm 1996-11-19 restored changed prettyprinting of ==>;
1996-11-18 wenzelm 1996-11-18 added add_modesyntax(_i); improved syntax of ==, =?=, ==> (now allows "op ..."); added Pure symbolfont syntax;
1996-11-14 wenzelm 1996-11-14 removed 'open Syntax Type';
1996-11-14 wenzelm 1996-11-14 subsig tuning;
1996-11-13 wenzelm 1996-11-13 tuned subsig;
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 paulson 1996-11-01 Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
1996-10-30 paulson 1996-10-30 Changed some mem calls to mem_string for greater efficiency (not that it could matter)
1996-10-15 paulson 1996-10-15 changed prettyprinting of ==>
1996-07-26 paulson 1996-07-26 Inserted spaces in error messages to improve readability
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-13 nipkow 1996-02-13 added nodup_Vars check in cterm_of. Prevents same var with distinct types.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-22 paulson 1995-12-22 "prep_const" now calls compress_type to ensure sharing among types of constants in theories.
1995-12-08 paulson 1995-12-08 exports exn_type_msg for error messages. Calls new infer_types. Improved comments.