| Thu, 17 May 2012 13:36:23 +0200 | blanchet | robustly parse Z3 4.0's output (with outcome appearing on first rather than last line) | changeset | files |
| Thu, 17 May 2012 13:36:23 +0200 | blanchet | added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter) | changeset | files |
| Wed, 16 May 2012 19:20:19 +0200 | kuncar | remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now | changeset | files |
| Wed, 16 May 2012 19:17:20 +0200 | kuncar | generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command | changeset | files |