| 2010-05-27 |
wenzelm |
2010-05-27 |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| 2010-03-09 |
wenzelm |
2010-03-09 |
aliases for class/type/const;
tuned;
|
file | diff | annotate |
| 2010-03-03 |
wenzelm |
2010-03-03 |
added extern_syntax;
|
file | diff | annotate |
| 2010-02-21 |
wenzelm |
2010-02-21 |
slightly more abstract syntax mark/unmark operations;
|
file | diff | annotate |
| 2010-02-21 |
wenzelm |
2010-02-21 |
authentic syntax for *all* term constants;
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
adapted Item_Net;
tuned;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
conceal consts via name space, not tags;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
maintain position of formal entities via name space;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
eliminated redundant bindings;
|
file | diff | annotate |
| 2009-07-09 |
wenzelm |
2009-07-09 |
renamed structure TermSubst to Term_Subst;
|
file | diff | annotate |
| 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);
|
file | diff | annotate |
| 2009-03-17 |
wenzelm |
2009-03-17 |
reverted abbreviations: improved performance via Item_Net.T;
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
renamed NameSpace.bind to NameSpace.define;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2009-03-08 |
wenzelm |
2009-03-08 |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2009-03-05 |
wenzelm |
2009-03-05 |
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2009-01-21 |
wenzelm |
2009-01-21 |
removed Ids;
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2008-12-30 |
ballarin |
2008-12-30 |
Temporarily avoid type errors in parse phase.
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-11-20 |
haftmann |
2008-11-20 |
using name bindings
|
file | diff | annotate |
| 2008-08-27 |
wenzelm |
2008-08-27 |
type Properties.T;
|
file | diff | annotate |
| 2008-02-10 |
wenzelm |
2008-02-10 |
maintain default position;
|
file | diff | annotate |
| 2007-11-11 |
wenzelm |
2007-11-11 |
simplified Consts.dest;
dest;
|
file | diff | annotate |
| 2007-11-11 |
wenzelm |
2007-11-11 |
renamed Symtab.update_list to Symtab.cons_list;
|
file | diff | annotate |
| 2007-10-20 |
wenzelm |
2007-10-20 |
PrintMode.internal;
|
file | diff | annotate |
| 2007-10-16 |
wenzelm |
2007-10-16 |
the_abbreviation: return plain rhs only;
force_expand: expand to plain rhs;
added revert_abbrev;
tuned;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2007-10-15 |
haftmann |
2007-10-15 |
prefer first constant component on merge
|
file | diff | annotate |
| 2007-10-12 |
haftmann |
2007-10-12 |
(intermediate quickfix)
|
file | diff | annotate |
| 2007-10-08 |
wenzelm |
2007-10-08 |
maintain typargs for abbrevs as well;
|
file | diff | annotate |
| 2007-09-30 |
wenzelm |
2007-09-30 |
maintain tags (Markup.property list);
tuned;
|
file | diff | annotate |
| 2007-09-22 |
wenzelm |
2007-09-22 |
certify: do_expand as explicit argument, actually certify type of abstractions;
tuned signature;
tuned;
|
file | diff | annotate |
| 2007-07-08 |
wenzelm |
2007-07-08 |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file | diff | annotate |
| 2007-05-24 |
haftmann |
2007-05-24 |
tuned Pure/General/name_space.ML
|
file | diff | annotate |
| 2007-04-02 |
paulson |
2007-04-02 |
exception handling
|
file | diff | annotate |
| 2006-12-13 |
wenzelm |
2006-12-13 |
tuned;
|
file | diff | annotate |
| 2006-12-12 |
wenzelm |
2006-12-12 |
abbreviate: tuned signature;
|
file | diff | annotate |
| 2006-12-09 |
wenzelm |
2006-12-09 |
abbreviate: always authentic, force expansion of internal abbreviations;
tuned signature;
tuned;
|
file | diff | annotate |
| 2006-12-07 |
wenzelm |
2006-12-07 |
tuned;
|
file | diff | annotate |
| 2006-12-06 |
wenzelm |
2006-12-06 |
abbreviate: improved error handling, return result;
|
file | diff | annotate |
| 2006-11-07 |
wenzelm |
2006-11-07 |
read_const: include type;
|
file | diff | annotate |
| 2006-11-05 |
wenzelm |
2006-11-05 |
added syntax_name;
|
file | diff | annotate |
| 2006-09-27 |
wenzelm |
2006-09-27 |
removed unused serial_of, name_of;
|
file | diff | annotate |
| 2006-09-21 |
wenzelm |
2006-09-21 |
serial numbers for consts;
added serial_of/name_of;
|
file | diff | annotate |
| 2006-09-15 |
wenzelm |
2006-09-15 |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file | diff | annotate |
| 2006-09-12 |
wenzelm |
2006-09-12 |
moved term subst functions to TermSubst;
|
file | diff | annotate |
| 2006-05-17 |
wenzelm |
2006-05-17 |
replaced early'' flag by inverted authentic'';
|
file | diff | annotate |
| 2006-05-17 |
wenzelm |
2006-05-17 |
always preserve authentic consts -- removed Syntax.mixfix_const;
|
file | diff | annotate |
| 2006-05-16 |
wenzelm |
2006-05-16 |
added syntax interface;
|
file | diff | annotate |
| 2006-05-05 |
wenzelm |
2006-05-05 |
extern_early: improved handling of undeclared constants;
|
file | diff | annotate |
| 2006-04-29 |
wenzelm |
2006-04-29 |
tuned;
|
file | diff | annotate |
| 2006-04-27 |
wenzelm |
2006-04-27 |
tuned basic list operators (flat, maps, map_filter);
|
file | diff | annotate |
| 2006-04-13 |
wenzelm |
2006-04-13 |
certify: ignore sort constraints of declarations (MAJOR CHANGE);
|
file | diff | annotate |