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;
2007-10-13 ago add_abbrevs: unvarify result;
2007-10-11 ago dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 ago tuned;
2007-10-11 ago replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-10 ago generalized notation interface (add or del);
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-09-30 ago add_consts_authentic/add_abbrev: tags ( list);
2007-09-29 ago removed obsolete external interface add_const_constraint;
2007-09-26 ago added minimize_sort, complete_sort;
2007-09-25 ago Syntax.parse/check/read;
2007-09-22 ago certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
2007-09-01 ago read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
2007-08-30 ago infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-20 ago read_def_terms: moved disambig to syntax.ML;
2007-08-14 ago replaced certify_typ_syntax/abbrev by certify_typ_mode;
2007-08-14 ago PrimitiveDefs.dest_def;
2007-08-12 ago read_def_terms': restrict scope of disambiguation to individual term;
2007-08-03 ago certify: no check_thy here;
2007-07-24 ago moved exception capture/release to structure Exn;
2007-07-09 ago type output = string indicates raw system output;
2007-07-07 ago simplified pretty token metric: type int;
2007-05-07 ago simplified DataFun interfaces;
2007-04-26 ago renamed some old names to;
2007-04-26 ago renamed some old names to;
2007-04-21 ago export get_sort (belongs to Syntax module);
2007-04-15 ago removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15 ago removed obsolete infer_types(_simult);
2007-04-14 ago read_typ_XXX: no sorts;
2007-01-19 ago moved ML translation interfaces to isar_cmd.ML;
2007-01-19 ago adapted ML context operations;
2006-12-29 ago replaced classes by all_classes (topologically sorted);
2006-12-12 ago add_abbrev: tuned signature;
2006-12-11 ago advanced translation functions: Proof.context;
2006-12-10 ago added no_frees;
2006-12-09 ago tuned Consts signature;
2006-12-07 ago simplified add_abbrev -- single argument;
2006-12-07 ago simplified add_abbrevs: no mixfix;
2006-12-06 ago add_abbrevs: moved common parts to consts.ML;