2008-06-21 ago added query_type/const/class (meta data);
2008-06-19 ago renamed is_abbrev_mode to abbrev_mode;
2008-06-18 ago simplified TypeInfer.infer_types;
2008-06-18 ago export transfer_syntax;
2008-06-13 ago map_const: soft version, no failure here;
2008-06-12 ago Facts.dest/export_static: content difference;
2008-05-18 ago unparse_term: check PureThy.old_appl_syntax instead of CPure;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago default token translations: observe Sign.is_pretty_global for fixed variables;
2008-04-22 ago exported is_abbrev mode discriminator
2008-04-18 ago print_cases: proper context for revert_skolem;
2008-04-17 ago revert_skolem: do not change non-reversible names;
2008-04-17 ago default token translations with proper markup;
2008-04-16 ago Facts.extern_static;
2008-04-16 ago removed obsolete valid_thms;
2008-04-15 ago Facts.intern, Facts.extern_table;
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-25 ago support dynamic facts;
2008-03-20 ago Facts.Named: include position;
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-18 ago valid_thms: get_thms_silent;
2008-03-17 ago Facts.add_local;
2008-03-15 ago replaced obsolete FactIndex.T by Facts.T;
2008-03-14 ago added mk_const functions
2008-03-11 ago put_thms: pass do_props;
2008-03-07 ago dropped local tsigs
2008-03-05 ago put_thms: do not index facts here (affects prems/this/calculation in particular);
2007-11-27 ago standard_parse_term: check ambiguous results without changing the result yet;
2007-11-23 ago explicit type signature
2007-11-21 ago intern_skolem: disallow qualified names;
2007-11-11 ago simplified Consts.dest;
2007-11-08 ago removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
2007-11-08 ago renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-07 ago export read_const';
2007-11-07 ago discontinued ProofContext.read_prop_legacy;
2007-11-06 ago read_const/legacy_intern_skolem: cover consts within the local scope;
2007-10-24 ago parse_term: invoke full Syntax.check_term, not just standard_infer_types;
2007-10-23 ago added XCONST syntax (keeps original spelling of const);
2007-10-21 ago context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});
2007-10-19 ago do not export standard_infer_types;
2007-10-16 ago exported standard_term_check
2007-10-16 ago Syntax.(un)check: explicit result option;
2007-10-16 ago added revert_abbrev;
2007-10-15 ago swapped constant components
2007-10-11 ago replaced Term.equiv_types by Type.similar_types;
2007-10-11 ago moved ProofContext.pp to Syntax.pp;
2007-10-10 ago generalized notation interface (add or del);
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-02 ago export tsig_of;
2007-09-30 ago add_abbrev: tags ( list);
2007-09-30 ago standard_term_check: include expand_abbrevs (back again);
2007-09-29 ago removed redundant const_constraint;
2007-09-29 ago exported constraint interfaces
2007-09-24 ago eliminated ProofContext.read_termTs;
2007-09-23 ago removed dead code;
2007-09-23 ago made smlnj happy;
2007-09-23 ago added read_term_pattern/schematic/abbrev;
2007-09-22 ago removed obsolete set_expand_abbrevs (superceded by mode_abbrev);