Tue, 24 Jun 2014 15:05:58 +0200 | Andreas Lochbihler | add lemma | changeset | files |
Tue, 24 Jun 2014 15:49:20 +0200 | blanchet | tuning | changeset | files |
Tue, 24 Jun 2014 15:08:19 +0200 | blanchet | optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct) | changeset | files |
Tue, 24 Jun 2014 14:56:08 +0200 | blanchet | minor table access optimization | changeset | files |
Tue, 24 Jun 2014 13:48:14 +0200 | desharna | document property 'rel_coinduct' | changeset | files |
Tue, 24 Jun 2014 13:48:14 +0200 | desharna | tune the implementation of 'rel_coinduct' | changeset | files |
Tue, 24 Jun 2014 13:48:14 +0200 | desharna | generate 'rel_coinduct' theorem for codatatypes | changeset | files |
Tue, 24 Jun 2014 13:48:14 +0200 | desharna | generate 'rel_coinduct0' theorem for codatatypes | changeset | files |