| Mon, 07 Jul 2014 16:06:46 +0200 | desharna | generate 'rel_cases' theorem for (co)datatypes | file | diff | annotate |
| Thu, 02 Jan 2014 09:50:22 +0100 | blanchet | don't generate any proof obligation for implicit (de facto) exclusiveness | file | diff | annotate |
| Sat, 21 Dec 2013 09:44:30 +0100 | blanchet | generate exhaust from nchotomy | file | diff | annotate |
| Mon, 09 Dec 2013 09:44:57 +0100 | blanchet | tuning -- moved ML files to subdirectory | file | diff | annotate | base |