Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | adapted examples to changes in SMT triggers | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | reduces Sledgehammer dependencies | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | eliminate dependency of SMT2 module on 'list' | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | tuning | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | removed subsumed record-related code, now that records are registered as 'ctr_sugar' | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | made lookup more robust in the face of missing (dummy) case constant | changeset | files |
Thu, 12 Jun 2014 01:00:49 +0200 | blanchet | use 'ctr_sugar' abstraction in SMT(2) | changeset | files |