Tue, 19 Aug 2014 14:58:38 +0200 | Andreas Lochbihler | Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e) | changeset | files |
Tue, 19 Aug 2014 09:39:11 +0200 | blanchet | reduced dependency on 'Datatype' theory and ML module | changeset | files |
Tue, 19 Aug 2014 09:36:57 +0200 | blanchet | removed Z3 3.2, now superseded by Z3 4.3 | changeset | files |
Tue, 19 Aug 2014 09:36:37 +0200 | blanchet | avoid old 'smt' method in examples | changeset | files |
Tue, 19 Aug 2014 09:34:57 +0200 | blanchet | robustified tactics | changeset | files |
Tue, 19 Aug 2014 09:34:41 +0200 | blanchet | tuning | changeset | files |