Fri, 19 Dec 2014 11:17:23 +0100 | desharna | generate 'case_distrib' for Ctr_Sugars | file | diff | annotate |
Wed, 08 Oct 2014 17:09:07 +0200 | wenzelm | added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N}; | file | diff | annotate |
Mon, 18 Aug 2014 17:19:58 +0200 | blanchet | reordered some (co)datatype property names for more consistency | file | diff | annotate |
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 |