src/Pure/consts.ML
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-03-17 wenzelm 2009-03-17 strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions);
2009-03-17 wenzelm 2009-03-17 reverted abbreviations: improved performance via Item_Net.T;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-10 wenzelm 2009-03-10 Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05 wenzelm 2009-03-05 eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-30 ballarin 2008-12-30 Temporarily avoid type errors in parse phase.
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-20 haftmann 2008-11-20 using name bindings
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-02-10 wenzelm 2008-02-10 maintain default position;
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest; dest;
2007-11-11 wenzelm 2007-11-11 renamed Symtab.update_list to Symtab.cons_list;
2007-10-20 wenzelm 2007-10-20 PrintMode.internal;
2007-10-16 wenzelm 2007-10-16 the_abbreviation: return plain rhs only; force_expand: expand to plain rhs; added revert_abbrev; tuned;
2007-10-15 wenzelm 2007-10-15 renamed the_declaration to the_type; added type_scheme, which covers proper consts and abbreviations (like typargs); tuned;
2007-10-15 haftmann 2007-10-15 prefer first constant component on merge
2007-10-12 haftmann 2007-10-12 (intermediate quickfix)
2007-10-08 wenzelm 2007-10-08 maintain typargs for abbrevs as well;
2007-09-30 wenzelm 2007-09-30 maintain tags (Markup.property list); tuned;
2007-09-22 wenzelm 2007-09-22 certify: do_expand as explicit argument, actually certify type of abstractions; tuned signature; tuned;
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-04-02 paulson 2007-04-02 exception handling
2006-12-13 wenzelm 2006-12-13 tuned;
2006-12-12 wenzelm 2006-12-12 abbreviate: tuned signature;
2006-12-09 wenzelm 2006-12-09 abbreviate: always authentic, force expansion of internal abbreviations; tuned signature; tuned;
2006-12-07 wenzelm 2006-12-07 tuned;
2006-12-06 wenzelm 2006-12-06 abbreviate: improved error handling, return result;
2006-11-07 wenzelm 2006-11-07 read_const: include type;
2006-11-05 wenzelm 2006-11-05 added syntax_name;
2006-09-27 wenzelm 2006-09-27 removed unused serial_of, name_of;
2006-09-21 wenzelm 2006-09-21 serial numbers for consts; added serial_of/name_of;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-12 wenzelm 2006-09-12 moved term subst functions to TermSubst;
2006-05-17 wenzelm 2006-05-17 replaced early'' flag by inverted authentic'';
2006-05-17 wenzelm 2006-05-17 always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-16 wenzelm 2006-05-16 added syntax interface;
2006-05-05 wenzelm 2006-05-05 extern_early: improved handling of undeclared constants;
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 certify: ignore sort constraints of declarations (MAJOR CHANGE);
2006-04-08 wenzelm 2006-04-08 added intern/extern/extern_early; added expand_abbrevs flag; strip_abss: demand ocurrences of bounds in body; const decl: added flag for early externing (disabled for authentic syntax); abbrevs: support print mode; major cleanup;
2006-02-17 wenzelm 2006-02-17 constrain: assert const declaration, optional type (i.e. may delete constraints);
2006-02-12 wenzelm 2006-02-12 added eq_consts; reverted abbrevs: try all abstraction prefixes;
2006-02-10 wenzelm 2006-02-10 abbrevs: store in reverted orientation; tuned;
2006-02-07 wenzelm 2006-02-07 renamed space to space_of; removed expansion; added abbrevs_of; added read_const; certify: substitute arguments into expanded const; tuned;
2006-02-06 wenzelm 2006-02-06 added abbreviations; added certify (mostly from sign.ML);
2005-11-14 wenzelm 2005-11-14 added instance;
2005-11-10 wenzelm 2005-11-10 uncurried Consts.typargs;
2005-11-08 wenzelm 2005-11-08 const args: do not store variable names (unused);
2005-11-02 wenzelm 2005-11-02 removed unused modify_typargs, map_typargs, fold_typargs;
2005-11-02 wenzelm 2005-11-02 Polymorphic constants.