Mon, 04 Nov 2013 14:46:38 +0100 |
blanchet |
more robust n2m w.r.t. 'let's
|
file |
diff |
annotate
|
Mon, 04 Nov 2013 10:52:41 +0100 |
blanchet |
handle constructor syntax in n2m primcorec
|
file |
diff |
annotate
|
Tue, 29 Oct 2013 12:13:00 +0100 |
panny |
include corecursive functions' arguments in callssss
|
file |
diff |
annotate
|
Sat, 26 Oct 2013 13:01:41 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sat, 26 Oct 2013 13:00:55 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sat, 26 Oct 2013 12:57:17 +0200 |
blanchet |
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
|
file |
diff |
annotate
|
Sat, 26 Oct 2013 12:54:57 +0200 |
blanchet |
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
|
file |
diff |
annotate
|
Sat, 26 Oct 2013 12:54:21 +0200 |
blanchet |
tuned error message
|
file |
diff |
annotate
|
Thu, 24 Oct 2013 19:43:21 +0200 |
blanchet |
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
|
file |
diff |
annotate
|
Thu, 24 Oct 2013 18:50:59 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 24 Oct 2013 18:37:54 +0200 |
blanchet |
more correct (!) types for recursive calls
|
file |
diff |
annotate
|
Mon, 21 Oct 2013 09:31:19 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 21 Oct 2013 08:27:51 +0200 |
blanchet |
more informative abort
|
file |
diff |
annotate
|
Mon, 21 Oct 2013 07:50:32 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 21 Oct 2013 07:24:18 +0200 |
blanchet |
systematically close derivations in BNF package
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 23:36:18 +0200 |
blanchet |
removed temporary error handling
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 23:29:49 +0200 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 22:51:21 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 22:39:40 +0200 |
blanchet |
reintroduced parts of 07a8145aaeba that a22ded8a7f7d wrongly took out
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 19:23:28 +0200 |
blanchet |
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 19:20:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 19:20:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 19:20:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 19:20:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 20 Oct 2013 18:22:59 +0200 |
blanchet |
simplify code
|
file |
diff |
annotate
|
Sat, 19 Oct 2013 00:00:50 +0200 |
blanchet |
improve support for recursion through functions
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 19:18:32 +0200 |
panny |
merge
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 19:03:39 +0200 |
panny |
generate callssss
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 18:58:46 +0200 |
blanchet |
set stage for more flexible 'primrec' syntax for recursion through functions
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 16:02:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 15:25:39 +0200 |
blanchet |
conceal more ugly constructions
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 15:19:21 +0200 |
blanchet |
conceal prim(co)rec definitions
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 15:12:04 +0200 |
blanchet |
avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
|
file |
diff |
annotate
|
Fri, 18 Oct 2013 10:35:56 +0200 |
blanchet |
make sure that registered code equations are actually equations
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 10:29:28 +0200 |
blanchet |
graceful handling of abort
|
file |
diff |
annotate
|
Thu, 17 Oct 2013 10:06:48 +0200 |
panny |
generalized interface
|
file |
diff |
annotate
|
Wed, 16 Oct 2013 20:44:33 +0200 |
panny |
use Code.abort instead of undefined in auto-generated equations
|
file |
diff |
annotate
|
Mon, 14 Oct 2013 10:55:49 +0200 |
blanchet |
keep temporary error handling in there until code equations are properly generated
|
file |
diff |
annotate
|
Mon, 14 Oct 2013 09:31:42 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
Mon, 14 Oct 2013 09:17:04 +0200 |
blanchet |
strengthened tactic w.r.t. "let"
|
file |
diff |
annotate
|
Fri, 11 Oct 2013 23:15:30 +0200 |
panny |
compile -- fix typo introduced in 07a8145aaeba
|
file |
diff |
annotate
|
Fri, 11 Oct 2013 20:47:37 +0200 |
panny |
pass the right theorems to tactic
|
file |
diff |
annotate
|
Fri, 11 Oct 2013 16:31:23 +0200 |
panny |
prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
|
file |
diff |
annotate
|
Mon, 07 Oct 2013 23:38:57 +0200 |
blanchet |
allow 'let's around constructors in constructor view
|
file |
diff |
annotate
|
Sun, 06 Oct 2013 20:24:06 +0200 |
blanchet |
generate optimized DNF formula
|
file |
diff |
annotate
|
Sun, 06 Oct 2013 20:24:05 +0200 |
blanchet |
rationalized negation code
|
file |
diff |
annotate
|
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
|