| 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
|
| Tue, 01 Oct 2013 14:05:25 +0200 |
blanchet |
renamed theory file
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 02:25:33 +0200 |
blanchet |
got rid of dependency on silly 'eq_ifI' theorem
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 02:09:52 +0200 |
blanchet |
more powerful/robust tactics
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 01:05:06 +0200 |
blanchet |
made tactic more flexible w.r.t. case expressions and such
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 10:53:09 +0200 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Thu, 19 Sep 2013 02:30:45 +0200 |
blanchet |
added helper function for code equations in primcorec
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 17:36:47 +0200 |
blanchet |
no need thanks to "Code.abort"
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 16:44:19 +0200 |
blanchet |
minor change related to code equations in primcorec
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:33:32 +0200 |
blanchet |
new tactics for constructor view
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 00:07:46 +0200 |
blanchet |
avoid a keyword
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:43:39 +0200 |
blanchet |
tuned theory name
|
file |
diff |
annotate
| base
|