src/Pure/sign.ML
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;
2008-06-13 wenzelm 2008-06-13 map_const: soft version, no failure here;
2008-05-23 wenzelm 2008-05-23 add constants: set Markup.theory_nameN in tags;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 added pretty_global flag;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T;
2008-04-15 wenzelm 2008-04-15 removed obsolete SIGN_THEORY -- no name aliases in structure Theory; simplified hide_XXX interfaces; moved hide_names to isar_cmd.ML;
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
2008-03-14 haftmann 2008-03-14 added mk_const functions
2007-11-27 wenzelm 2007-11-27 standard_parse_term: check ambiguous results without changing the result yet;
2007-11-23 haftmann 2007-11-23 separated typedecl module, providing typedecl command with interpretation
2007-11-11 wenzelm 2007-11-11 syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-10 wenzelm 2007-11-10 notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-09 wenzelm 2007-11-09 tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-08 wenzelm 2007-11-08 removed unused read_def_terms';
2007-11-07 wenzelm 2007-11-07 removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-10-20 wenzelm 2007-10-20 no_variables: tuned error msg;
2007-10-17 wenzelm 2007-10-17 removed unused set_policy;
2007-10-16 wenzelm 2007-10-16 add_abbrev: removed Logic.legacy_varifyT, do not unvarify result (again); added revert_abbrev;
2007-10-15 wenzelm 2007-10-15 renamed Consts.the_declaration to Consts.the_type;
2007-10-13 wenzelm 2007-10-13 add_abbrevs: unvarify result;
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 tuned;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML);
2007-09-30 wenzelm 2007-09-30 add_consts_authentic/add_abbrev: tags (Markup.property list); tuned signature;
2007-09-29 wenzelm 2007-09-29 removed obsolete external interface add_const_constraint; removed redundant const_constraint; renamed add_const_constraint_i to add_const_constraint;
2007-09-26 wenzelm 2007-09-26 added minimize_sort, complete_sort;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-22 wenzelm 2007-09-22 certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
2007-09-01 wenzelm 2007-09-01 read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
2007-08-30 wenzelm 2007-08-30 infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-20 wenzelm 2007-08-20 read_def_terms: moved disambig to syntax.ML;