src/HOL/Tools/SMT/smt_util.ML
24 months ago blanchet 2017-08-29 towards support for HO SMT-LIB
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 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 clarified signature;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'