src/HOL/Tools/SMT/smtlib_isar.ML
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2014-09-29 blanchet 2014-09-29 support hypotheses with schematics in Isar proofs
2014-08-28 blanchet 2014-08-28 keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'