src/Pure/Proof/proof_checker.ML
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
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-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-03-15 wenzelm 2014-03-15 tuned signature; eliminated clones;
2011-09-19 wenzelm 2011-09-19 fixed headers;
2011-08-08 wenzelm 2011-08-08 modernized file proof_checker.ML;