2015-04-09 wenzelm 2015-04-09 make SML/NJ more happy;
2015-03-29 wenzelm 2015-03-29 tuned;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-13 hoelzl 2015-01-13 measurability prover: removed app splitting, replaced by more powerful destruction rules
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-24 hoelzl 2014-11-24 cleanup measurability prover
2014-11-11 Andreas Lochbihler 2014-11-11 add del option to measurable; make measurability rules available as dynamic theorem;
2014-04-09 wenzelm 2014-04-09 proper context for print_tac;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-08-16 wenzelm 2013-08-16 more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file