src/Pure/sign.ML
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.
1995-09-01 clasohm 1995-09-01 added same_sg and same_thm
1995-09-01 wenzelm 1995-09-01 nonempty_sort: no longer var names as args;
1995-08-01 wenzelm 1995-08-01 added (my own version of) nonempty_sort: sg -> (string * sort) list -> sort -> bool;
1995-08-01 nipkow 1995-08-01 Added nonempty_sort.
1995-07-07 clasohm 1995-07-07 moved mixfix syntax to Syntax/mixfix.ML
1995-07-03 clasohm 1995-07-03 added cargs for curried function application
1995-06-26 wenzelm 1995-06-26 added add_trrules_i;
1995-03-30 clasohm 1995-03-30 changed pretty printing of applC
1995-03-17 nipkow 1995-03-17 Corrected a silly old bug in merge_tsigs. Rewrote a lot of Nimmermann's code.
1995-03-15 clasohm 1995-03-15 removed print_msg parameter of infer_types
1995-03-14 nipkow 1995-03-14 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1995-03-03 clasohm 1995-03-03 fixed a bug in infer_types/exn_type_msg
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-02-17 clasohm 1995-02-17 added check "length ts > 1" before printing ambiguity warning in infer_types
1995-01-27 clasohm 1995-01-27 moved ambiguity_level to Syntax/syntax.ML
1995-01-26 clasohm 1995-01-26 added reference variable ambiguity_level to control ambiguity warnings
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
1994-12-08 clasohm 1994-12-08 replaced type_syn by pure_syn in Pure signature
1994-11-02 lcp 1994-11-02 Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of exception TYPE
1994-10-04 clasohm 1994-10-04 added print_msg; added call of Type.infer_types to resolve ambiguities
1994-09-26 wenzelm 1994-09-26 exported pretty_sort; various minor internal changes;
1994-09-06 wenzelm 1994-09-06 minor internal changes;
1994-08-23 wenzelm 1994-08-23 removed constant _constrain from Pure sig;
1994-08-19 wenzelm 1994-08-19 added pretty_sg; added infer_types; removed subclasses arg of add_classes; removed old 'extend' and related stuff; various minor internal changes;
1994-06-16 wenzelm 1994-06-16 added add_classrel;
1994-06-09 wenzelm 1994-06-09 workaround bug in Type.expand_typ;
1994-06-01 wenzelm 1994-06-01 replaced infix also by |>
1994-05-26 wenzelm 1994-05-26 added subsort, norm_sort, classes; minor internal cleanups;
1994-05-19 wenzelm 1994-05-19 added const_type: sg -> typ option; stamps now stored in REVERSE order; now supports 'draft signatures' and incremental extension: is_draft, add_classes (supports axclasses), add_defsort, add_types, add_tyabbrs, add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i, add_trfuns, add_trrules, add_name, make_draft; added const_of_class, class_of_const (for axclasses); changed the pure signature to support axclasses (added itself, TYPE); various major internal changes;
1994-03-04 wenzelm 1994-03-04 fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;