| 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
|
| Fri, 17 Feb 2006 20:03:10 +0100 |
wenzelm |
constrain: assert const declaration, optional type (i.e. may delete constraints);
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:21 +0100 |
wenzelm |
added eq_consts;
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:24 +0100 |
wenzelm |
abbrevs: store in reverted orientation;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:47 +0100 |
wenzelm |
renamed space to space_of;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:02 +0100 |
wenzelm |
added abbreviations;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2005 14:37:38 +0100 |
wenzelm |
added instance;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:16 +0100 |
wenzelm |
uncurried Consts.typargs;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:43:08 +0100 |
wenzelm |
const args: do not store variable names (unused);
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:48:55 +0100 |
wenzelm |
removed unused modify_typargs, map_typargs, fold_typargs;
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:46:56 +0100 |
wenzelm |
Polymorphic constants.
|
file |
diff |
annotate
|