| Wed, 02 Oct 2013 15:13:41 +0200 |
traytel |
made SML/NJ happy
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 17:04:27 +0200 |
traytel |
improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.)
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 22:36:43 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 18:08:35 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 17:53:44 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 16:25:12 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 16:10:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 13:51:08 +0200 |
blanchet |
use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 10:57:39 +0200 |
blanchet |
strengthen tactic
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 10:26:00 +0200 |
blanchet |
use needed case theorems
|
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:07 +0200 |
blanchet |
tuning
|
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 21:25:53 +0200 |
panny |
simplified code
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
thread through bound types
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
killed redundant argument
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 14:21:18 +0200 |
blanchet |
move useful functions to library
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 13:39:34 +0200 |
panny |
merge
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 12:43:20 +0200 |
panny |
simplified code
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 00:38:13 +0200 |
panny |
add non-corecursive constructor view theorems to simps
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 12:29:06 +0200 |
blanchet |
more powerful fold
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 22:21:51 +0200 |
blanchet |
commented out debugging output in "primcorec"
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 20:40:36 +0200 |
blanchet |
started adding support for "nat_case" as case study for all "case" constructs
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 18:07:09 +0200 |
panny |
support "of" syntax to disambiguate selector equations
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 17:54:09 +0200 |
blanchet |
don't note more induction principles than there are functions + tuning
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 15:16:59 +0200 |
panny |
add "primcorec" command (cf. ae7f50e70c09)
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:18:22 +0200 |
blanchet |
set code and nitpick_simp attributes on primcorec theorems
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:58:37 +0200 |
blanchet |
note coinduct theorems in "primcorec"
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:45:26 +0200 |
blanchet |
generate "simps" from "primcorec"
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 10:38:23 +0200 |
blanchet |
undid copy-paste
|
file |
diff |
annotate
|