src/HOL/Tools/SMT/z3_isar.ML
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2014-11-19 blanchet 2014-11-19 removed redundant code line
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'