src/Pure/sign.ML
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;
1994-02-09 wenzelm 1994-02-09 *** empty log message ***
1994-02-08 wenzelm 1994-02-08 improved eq_sg; cosmetical change in print_sg;
1994-02-03 wenzelm 1994-02-03 major cleanup; added eq_sig; added print_sg (full contents), pprint_sg (stamps only); added certify_typ, certify_term; changed read_typ: result now certified;
1994-01-18 lcp 1994-01-18 Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.
1994-01-11 nipkow 1994-01-11 moved misplaced comment
1994-01-04 nipkow 1994-01-04 added fake_cterm_of to speed up rewriting
1993-12-30 nipkow 1993-12-30 added subsig: sg * sg -> bool to test if one signature is contained in another.
1993-12-21 nipkow 1993-12-21 Necessary changes to accomodate type abbreviations.
1993-12-14 nipkow 1993-12-14 Updated read_insts to approximate simultaneous type checking of substitution pairs.
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-29 wenzelm 1993-11-29 extend: cleaned up, adapted for new Syntax.extend; extend, merge: improved roots (logical_types) handling;
1993-11-25 nipkow 1993-11-25 changed some names and deleted *NORMALIZED*
1993-11-25 wenzelm 1993-11-25 Sign.extend: Syntax.extend now called with read_ty;
1993-10-04 wenzelm 1993-10-04 Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs;
1993-09-16 clasohm 1993-09-16 Initial revision