Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc. | changeset | files |
Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | moved skolem method | changeset | files |
Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | added 'skolem' method, esp. for 'obtain's generated from Z3 proofs | changeset | files |