| Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 22:50:35 +0100 |
wenzelm |
added extern_syntax;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 21:08:25 +0100 |
wenzelm |
authentic syntax for *all* term constants;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 20:59:34 +0100 |
wenzelm |
adapted Item_Net;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:18:35 +0100 |
wenzelm |
conceal consts via name space, not tags;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 21:30:33 +0200 |
wenzelm |
maintain position of formal entities via name space;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 16:55:21 +0100 |
wenzelm |
reverted abbreviations: improved performance via Item_Net.T;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 15:27:07 +0100 |
wenzelm |
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Tue, 30 Dec 2008 08:18:54 +0100 |
ballarin |
Temporarily avoid type errors in parse phase.
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2008 20:49:42 +0100 |
wenzelm |
maintain default position;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 20:29:04 +0100 |
wenzelm |
simplified Consts.dest;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:00:08 +0100 |
wenzelm |
renamed Symtab.update_list to Symtab.cons_list;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 18:54:29 +0200 |
wenzelm |
PrintMode.internal;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 17:06:09 +0200 |
wenzelm |
the_abbreviation: return plain rhs only;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 21:08:35 +0200 |
wenzelm |
renamed the_declaration to the_type;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:41 +0200 |
haftmann |
prefer first constant component on merge
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 14:42:29 +0200 |
haftmann |
(intermediate quickfix)
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 18:13:08 +0200 |
wenzelm |
maintain typargs for abbrevs as well;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:34 +0200 |
wenzelm |
maintain tags (Markup.property list);
|
file |
diff |
annotate
|
| Sat, 22 Sep 2007 17:45:55 +0200 |
wenzelm |
certify: do_expand as explicit argument, actually certify type of abstractions;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:37 +0200 |
haftmann |
tuned Pure/General/name_space.ML
|
file |
diff |
annotate
|
| Mon, 02 Apr 2007 11:29:44 +0200 |
paulson |
exception handling
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:47:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:21 +0100 |
wenzelm |
abbreviate: tuned signature;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:39 +0100 |
wenzelm |
abbreviate: always authentic, force expansion of internal abbreviations;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:44 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:18:57 +0100 |
wenzelm |
abbreviate: improved error handling, return result;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:46:47 +0100 |
wenzelm |
read_const: include type;
|
file |
diff |
annotate
|
| Sun, 05 Nov 2006 21:44:34 +0100 |
wenzelm |
added syntax_name;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 21:13:09 +0200 |
wenzelm |
removed unused serial_of, name_of;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:43 +0200 |
wenzelm |
serial numbers for consts;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 12:12:46 +0200 |
wenzelm |
moved term subst functions to TermSubst;
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:34:45 +0200 |
wenzelm |
replaced early'' flag by inverted authentic'';
|
file |
diff |
annotate
|
| Wed, 17 May 2006 01:23:46 +0200 |
wenzelm |
always preserve authentic consts -- removed Syntax.mixfix_const;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:05 +0200 |
wenzelm |
added syntax interface;
|
file |
diff |
annotate
|
| Fri, 05 May 2006 21:59:44 +0200 |
wenzelm |
extern_early: improved handling of undeclared constants;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:11 +0200 |
wenzelm |
certify: ignore sort constraints of declarations (MAJOR CHANGE);
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:17 +0200 |
wenzelm |
added intern/extern/extern_early;
|
file |
diff |
annotate
|