Fri, 04 Oct 2013 18:27:07 +0200 |
panny |
process code-style inputs
|
file |
diff |
annotate
|
Wed, 02 Oct 2013 22:54:42 +0200 |
blanchet |
strengthened tactic (primcorec_sel_tac) + tuning
|
file |
diff |
annotate
|
Wed, 02 Oct 2013 16:29:40 +0200 |
blanchet |
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
|
file |
diff |
annotate
|
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
|
Mon, 23 Sep 2013 10:34:10 +0200 |
blanchet |
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 10:30:43 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 16:32:27 +0200 |
blanchet |
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 00:08:42 +0200 |
blanchet |
setting the stage for safe constructor simp rules
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 23:54:54 +0200 |
blanchet |
added TODO
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 17:38:03 +0200 |
traytel |
don't declare ctr view primcorec theorems as simp (they loop)
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 16:12:43 +0200 |
panny |
simplified code; eliminated some dummyTs
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 12:20:12 +0200 |
blanchet |
avoid infinite loop for unapplied terms + tuning
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 11:27:32 +0200 |
blanchet |
generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 01:09:25 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 00:32:33 +0200 |
panny |
generate more theorems (e.g. for types with only one constructor)
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 22:59:11 +0200 |
panny |
generate constructor view theorems
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 18:12:40 +0200 |
blanchet |
tuned tactics
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 15:33:32 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 16 Sep 2013 15:03:23 +0200 |
panny |
prove simp theorems for newly generated definitions
|
file |
diff |
annotate
|
Thu, 05 Sep 2013 01:58:48 +0200 |
panny |
support indirect corecursion
|
file |
diff |
annotate
|
Wed, 04 Sep 2013 02:11:50 +0200 |
panny |
various refactoring;
|
file |
diff |
annotate
|
Mon, 02 Sep 2013 15:13:00 +0200 |
panny |
handle direct corecursion
|
file |
diff |
annotate
|
Sun, 01 Sep 2013 14:00:05 +0200 |
panny |
improved interfaces
|
file |
diff |
annotate
|
Sun, 01 Sep 2013 10:45:54 +0200 |
panny |
simplified rewriting of map arguments
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 23:55:03 +0200 |
traytel |
merged
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 23:49:14 +0200 |
traytel |
honor mixfix specifications
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 20:37:31 +0200 |
panny |
simplified recursive calls' replacement
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 18:18:33 +0200 |
panny |
handle selector formulae with no corecursive calls
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 21:43:15 +0200 |
panny |
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 14:17:19 +0200 |
blanchet |
more canonical naming
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 12:37:03 +0200 |
blanchet |
moved keywords down the hierarchy
|
file |
diff |
annotate
|