src/Tools/misc_legacy.ML
2015-06-02 wenzelm 2015-06-02 clarified context;
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;
2014-12-21 wenzelm 2014-12-21 proper context;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-14 wenzelm 2014-03-14 prefer more robust Synchronized.var;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-03-14 wenzelm 2013-03-14 tuned signature;
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-03-19 wenzelm 2012-03-19 moved some legacy stuff;
2012-03-13 wenzelm 2012-03-13 more explicit indication of def names;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-12-14 wenzelm 2011-12-14 eliminated dead code;
2011-10-19 wenzelm 2011-10-19 tuned legacy signature;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;