Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | added appropriate method for skolemization of Z3 steps to the mix | changeset | files |
Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared) | changeset | files |
Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | honor 'try0' also for one-liners | changeset | files |