| Wed, 08 Apr 2015 19:39:08 +0200 | wenzelm | proper context for Object_Logic operations; | file | diff | annotate |
| Mon, 29 Sep 2014 20:26:04 +0200 | blanchet | support hypotheses with schematics in Isar proofs | file | diff | annotate |
| 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 |