| Tue, 14 Jan 2014 18:41:24 +0100 | blanchet | use 'disc_exhausts' property both from types on which 'case's take place and on return type | changeset | files |
| Mon, 13 Jan 2014 20:20:44 +0100 | wenzelm | activation of Z3 via "z3_non_commercial" system option (without requiring restart); | changeset | files |
| Mon, 13 Jan 2014 18:47:48 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 13 Jan 2014 14:11:02 +0100 | blanchet | use the right context in 'unfold_thms id_def' | changeset | files |