src/Pure/consts.ML
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Wed, 13 Jul 2011 20:36:18 +0200 wenzelm sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
Sat, 23 Apr 2011 18:46:01 +0200 wenzelm clarified Consts.read_const;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Fri, 17 Dec 2010 22:23:56 +0100 wenzelm extra checking of name bindings for classes, types, consts;
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
Thu, 27 May 2010 18:10:37 +0200 wenzelm renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
Tue, 09 Mar 2010 23:29:04 +0100 wenzelm aliases for class/type/const;
Wed, 03 Mar 2010 22:50:35 +0100 wenzelm added extern_syntax;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:08:25 +0100 wenzelm authentic syntax for *all* term constants;
Sun, 01 Nov 2009 20:59:34 +0100 wenzelm adapted Item_Net;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sun, 25 Oct 2009 13:18:35 +0100 wenzelm conceal consts via name space, not tags;
Sat, 24 Oct 2009 21:30:33 +0200 wenzelm maintain position of formal entities via name space;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:20:03 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Tue, 17 Mar 2009 19:53:57 +0100 wenzelm 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);
Tue, 17 Mar 2009 16:55:21 +0100 wenzelm reverted abbreviations: improved performance via Item_Net.T;
Thu, 12 Mar 2009 11:10:02 +0100 wenzelm renamed NameSpace.bind to NameSpace.define;
Tue, 10 Mar 2009 22:49:56 +0100 wenzelm Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 17:35:37 +0100 wenzelm Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
Thu, 05 Mar 2009 15:27:07 +0100 wenzelm eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Tue, 30 Dec 2008 08:18:54 +0100 ballarin Temporarily avoid type errors in parse phase.
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 20 Nov 2008 14:55:25 +0100 haftmann using name bindings
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Sun, 10 Feb 2008 20:49:42 +0100 wenzelm maintain default position;
Sun, 11 Nov 2007 20:29:04 +0100 wenzelm simplified Consts.dest;
Sun, 11 Nov 2007 14:00:08 +0100 wenzelm renamed Symtab.update_list to Symtab.cons_list;
Sat, 20 Oct 2007 18:54:29 +0200 wenzelm PrintMode.internal;
Tue, 16 Oct 2007 17:06:09 +0200 wenzelm the_abbreviation: return plain rhs only;
Mon, 15 Oct 2007 21:08:35 +0200 wenzelm renamed the_declaration to the_type;
Mon, 15 Oct 2007 15:29:41 +0200 haftmann prefer first constant component on merge
Fri, 12 Oct 2007 14:42:29 +0200 haftmann (intermediate quickfix)
Mon, 08 Oct 2007 18:13:08 +0200 wenzelm maintain typargs for abbrevs as well;
Sun, 30 Sep 2007 16:20:34 +0200 wenzelm maintain tags (Markup.property list);
Sat, 22 Sep 2007 17:45:55 +0200 wenzelm certify: do_expand as explicit argument, actually certify type of abstractions;
Sun, 08 Jul 2007 19:51:58 +0200 wenzelm replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Thu, 24 May 2007 08:37:37 +0200 haftmann tuned Pure/General/name_space.ML
Mon, 02 Apr 2007 11:29:44 +0200 paulson exception handling
Wed, 13 Dec 2006 15:47:31 +0100 wenzelm tuned;
Tue, 12 Dec 2006 20:49:21 +0100 wenzelm abbreviate: tuned signature;
Sat, 09 Dec 2006 18:05:39 +0100 wenzelm abbreviate: always authentic, force expansion of internal abbreviations;
Thu, 07 Dec 2006 17:58:44 +0100 wenzelm tuned;
Wed, 06 Dec 2006 21:18:57 +0100 wenzelm abbreviate: improved error handling, return result;
less more (0) -60 tip