src/HOL/Tools/TFL/dcterm.ML
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 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-01-16 wenzelm 2011-01-16 tuned headers;
2010-12-15 wenzelm 2010-12-15 avoid ML structure aliases (especially single-letter abbreviations);
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-19 haftmann 2010-08-19 corrected some long-overseen misperceptions in recdef
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;