| Mon, 13 Sep 2010 11:13:15 +0200 | nipkow | renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI | changeset | files |
| Mon, 13 Sep 2010 08:43:48 +0200 | nipkow | added and renamed lemmas | changeset | files |
| Mon, 13 Sep 2010 09:29:43 +0200 | bulwahn | merged | changeset | files |
| Fri, 10 Sep 2010 17:53:25 +0200 | bulwahn | directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory | changeset | files |
| Mon, 13 Sep 2010 06:02:47 +0200 | boehmes | added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet | changeset | files |
| Fri, 10 Sep 2010 23:56:35 +0200 | krauss | use eta-contracted version for occurrence check (avoids possible non-termination) | changeset | files |
| Mon, 13 Sep 2010 13:20:18 +0200 | wenzelm | tuned signature; | changeset | files |