Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | more rational unskolemizing of names | changeset | files |
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 |