2010-01-04 ago discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 ago dropped copy operation for legacy TheoryDataFun
2009-11-17 ago uniform new_group/reset_group;
2009-11-02 ago modernized structure Primitive_Defs;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago maintain theory name via name space, not tags;
2009-10-25 ago more direct access to naming;
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 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-09-30 ago removed redundant Sign.certify_prop, use Sign.cert_prop instead;
2009-07-06 ago witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-14 ago removed obsolete no_base_names naming policy;
2009-03-12 ago renamed sticky_prefix to mandatory_path;
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-11 ago removed obsolete absolute_path -- use root_path with qualified binding;
2009-03-10 ago explicit root_path, parent_path;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 ago replace old bstring by binding for logical primitives: class, type, const etc.;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Binding.str_of;
2009-02-27 ago eliminated NJ's List.nth;
2009-01-21 ago removed Ids;
2009-01-21 ago binding is alias for Binding.T
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module
2008-11-20 ago dropped legacy naming code
2008-11-20 ago using name bindings
2008-11-14 ago namify and name_decl combinators
2008-09-03 ago declare_const: Name.binding, store/report position;
2008-08-27 ago type Properties.T;
2008-06-20 ago type constructors now with markup
2008-06-19 ago moved get_sort to Isar/proof_context.ML;
2008-06-18 ago removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
2008-06-14 ago certify_term: reject qualified frees;
2008-06-13 ago map_const: soft version, no failure here;
2008-05-23 ago add constants: set Markup.theory_nameN in tags;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago added pretty_global flag;
2008-04-17 ago token translations: context dependent, result Pretty.T;
2008-04-15 ago removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
2008-04-13 ago tsig: removed unnecessary universal witness;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-14 ago added mk_const functions
2007-11-27 ago standard_parse_term: check ambiguous results without changing the result yet;
2007-11-23 ago separated typedecl module, providing typedecl command with interpretation
2007-11-11 ago syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-10 ago notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-09 ago tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-08 ago removed unused read_def_terms';
2007-11-07 ago removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-20 ago no_variables: tuned error msg;
2007-10-17 ago removed unused set_policy;
2007-10-16 ago add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again);
2007-10-15 ago renamed Consts.the_declaration to Consts.the_type;