2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 modernized/simplified Sign.set_defsort;
2010-04-16 wenzelm 2010-04-16 replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;
2010-04-15 wenzelm 2010-04-15 misc tuning and simplification;
2010-03-27 wenzelm 2010-03-27 disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 wenzelm 2010-03-15 tuned;
2010-03-15 wenzelm 2010-03-15 moved old Sign.intern_term to the place where it is still used;
2010-03-09 wenzelm 2010-03-09 aliases for class/type/const; tuned;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2010-02-27 wenzelm 2010-02-27 read_class: perform actual read, with source position;
2010-02-25 wenzelm 2010-02-25 provide direct access to the different kinds of type declarations;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-18 wenzelm 2010-02-18 more systematic treatment of qualified names derived from binding;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-01-04 wenzelm 2010-01-04 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 haftmann 2010-01-04 dropped copy operation for legacy TheoryDataFun
2009-11-17 wenzelm 2009-11-17 uniform new_group/reset_group; tuned signature;
2009-11-02 wenzelm 2009-11-02 modernized structure Primitive_Defs;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
2009-10-25 wenzelm 2009-10-25 more direct access to naming; tuned signature;
2009-10-25 wenzelm 2009-10-25 allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 wenzelm 2009-10-24 maintain position of formal entities via name space;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-09-30 wenzelm 2009-09-30 removed redundant Sign.certify_prop, use Sign.cert_prop instead; tuned;
2009-07-06 wenzelm 2009-07-06 witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-14 wenzelm 2009-03-14 removed obsolete no_base_names naming policy;
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-11 wenzelm 2009-03-11 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 wenzelm 2009-03-11 removed obsolete absolute_path -- use root_path with qualified binding;
2009-03-10 wenzelm 2009-03-10 explicit root_path, parent_path; derived absolute_path; tuned;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 replace old bstring by binding for logical primitives: class, type, const etc.;
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;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-03-03 wenzelm 2009-03-03 Binding.str_of;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-20 haftmann 2008-11-20 dropped legacy naming code
2008-11-20 haftmann 2008-11-20 using name bindings
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-09-03 wenzelm 2008-09-03 declare_const: Name.binding, store/report position;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-06-19 wenzelm 2008-06-19 moved get_sort to Isar/proof_context.ML; removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;
2008-06-18 wenzelm 2008-06-18 removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
2008-06-14 wenzelm 2008-06-14 certify_term: reject qualified frees;