| Thu, 28 Aug 2014 00:40:38 +0200 | blanchet | keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof | file | diff | annotate |
| Thu, 28 Aug 2014 00:40:38 +0200 | blanchet | renamed new SMT module from 'SMT2' to 'SMT' | file | diff | annotate | base |