Wed, 30 Jul 2014 10:50:30 +0200 | desharna | document property 'set_induct' | changeset | files |
Wed, 30 Jul 2014 10:50:28 +0200 | desharna | generate 'set_induct' theorem for codatatypes | changeset | files |
Wed, 30 Jul 2014 00:50:41 +0200 | blanchet | also try 'metis' with 'full_types' | changeset | files |