Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b" | changeset | files |
Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | SPASS-Pirate is now called Pirate | changeset | files |
Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | avoid duplicate simp warning for datatypes with explicit products | changeset | files |