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);
2007-09-17 ago avoid direct access to print_mode;
2007-09-01 ago removed unused join_mode;
2007-09-01 ago removed obsolete read/cert variations (cf.;
2007-08-31 ago reject_vars: accept type-inference params;
2007-08-31 ago export various inner syntax modes;
2007-08-30 ago added join_mode;
2007-08-30 ago moved type_mode to type.ML;
2007-08-21 ago added inner syntax mode, includes former type_mode and is_stmt;
2007-08-20 ago inner syntax: added parse_term/prop;
2007-08-20 ago prepare_dummies: NAMED_CRITICAL;
2007-08-14 ago added implicit type mode (cf. Type.mode);
2007-07-27 ago get_thm etc.: map empty name to dummy_thm;
2007-07-23 ago marked some CRITICAL sections (for multithreading);
2007-06-13 ago tuned msg;
2007-06-02 ago moved specific target/local_abbrev to theory_target.ML;
2007-05-08 ago simplified pretty_thm(_legacy);
2007-05-08 ago legacy_intern_skolem: legacy_feature;
2007-05-07 ago simplified DataFun interfaces;
2007-04-23 ago sane version of read_termTs (proper freeze);
2007-04-21 ago added decode_term (belongs to Syntax module);