2011-11-08 ago entity markup for bound variables;
2011-06-27 ago ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-05-03 ago more conventional naming scheme: names_long, names_short, names_unique;
2011-04-27 ago more informative markup for fixed variables (via name space entry);
2011-04-27 ago export Name_Space.entry_ord;
2011-04-23 ago added Name_Space.check/get convenience;
2011-04-17 ago tuned signature;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-11 ago Name_Space.entry_markup: keep def position as separate properties;
2011-03-27 ago decode_term: some context-sensitive markup;
2010-12-17 ago extra checking of name bindings for classes, types, consts;
2010-03-09 ago added Name_Space.alias -- additional accesses for an existing entry;
2010-03-03 ago removed unused external_names;
2010-02-18 ago more systematic treatment of qualified names derived from binding;
2009-11-17 ago uniform new_group/reset_group;
2009-10-28 ago let naming transform binding beforehand -- covering only the "conceal" flag for now;
2009-10-25 ago Name_Space.naming: maintain group and theory_name as well;
2009-10-25 ago allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 ago maintain position of formal entities via name space;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago maintain abstract entry, with position, identity etc.;
2009-10-21 ago curried inter as canonical list operation (beware of argument order)
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-03-14 ago removed obsolete no_base_names naming policy;
2009-03-12 ago renamed sticky_prefix to mandatory_path;
2009-03-12 ago renamed bind to define;
2009-03-11 ago eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-10 ago add_path: discontinued special meaning of "//", "/", "..";
2009-03-10 ago just one naming policy based on binding content -- eliminated odd "object-oriented" style;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-05 ago adapted Binding.dest;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago eliminated internal stamp equality, replaced by bare-metal pointer_eq;
2009-03-03 ago moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
2009-03-03 ago moved name space externalization flags back to name_space.ML;
2009-03-03 ago reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
2009-02-09 ago Nicer names in FindTheorems.
2009-01-21 ago binding is alias for Binding.T
2009-01-03 ago separator, is_qualified
2008-12-05 ago removed Table.extend, NameSpace.extend_table
2008-12-05 ago dropped NameSpace.declare_base
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module
2008-12-01 ago exported get_accesses (for diagnostic purpose)
2008-11-20 ago name spaces and name bindings
2008-06-13 ago hide: delete all accesses from extra names -- reduces ambiguity in extern;
2008-04-15 ago merge: canonical order;
2008-03-27 ago tuned comments;
2007-10-29 ago export is_hidden;
2007-10-17 ago store external accesses within name space (as produced by naming policy);
2007-08-20 ago tuned signature;
2007-07-09 ago declare: disallow quote (") in names;
2007-05-24 ago tuned Pure/General/name_space.ML
2007-01-10 ago removed NameSpace.split -- use qualifier/base instead;