2016-12-28 wenzelm 2016-12-28 more uniform treatment of "bad" like other messages (with serial number);
2016-12-13 wenzelm 2016-12-13 more symbols;
2015-10-30 wenzelm 2015-10-30 tuned signature -- clarified modules;
2015-07-28 wenzelm 2015-07-28 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;