Sat, 21 Dec 2013 09:44:30 +0100 | blanchet | generate exhaust from nchotomy | file | diff | annotate |
Sat, 21 Dec 2013 09:44:29 +0100 | blanchet | made tactic work with theorems with multiple assumptions | file | diff | annotate |
Sat, 21 Dec 2013 09:44:28 +0100 | blanchet | renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package) | file | diff | annotate |
Thu, 19 Dec 2013 21:49:30 +0100 | blanchet | implemented 'exhaustive' option in tactic | file | diff | annotate |
Sun, 01 Dec 2013 19:32:57 +0100 | panny | more work towards "exhaustive" | file | diff | annotate |
Wed, 06 Nov 2013 13:00:45 +0100 | blanchet | removed dead code | file | diff | annotate |
Mon, 04 Nov 2013 16:53:43 +0100 | blanchet | split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec') | file | diff | annotate | base |