| Mon, 12 Sep 2016 23:17:55 +0200 |
blanchet |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
file |
diff |
annotate
|
| Tue, 30 Aug 2016 09:04:40 +0200 |
traytel |
generate proper goal when equation is entered programmatically
|
file |
diff |
annotate
|
| Tue, 23 Aug 2016 15:19:32 +0200 |
traytel |
tuned signature
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 13:44:50 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 07:57:02 +0100 |
blanchet |
export ML function
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 19:15:06 +0100 |
blanchet |
don't throw an exception when trying to print an error message
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 18:32:12 +0100 |
blanchet |
eta-expansion done right in "primcorec"
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 10:02:12 +0100 |
traytel |
respect qualification when noting theorems in prim(co)rec
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:47:35 +0100 |
blanchet |
clearer error message
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:02:43 +0200 |
blanchet |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 12:01:07 +0200 |
traytel |
collect the names from goals in favor of fragile exports
|
file |
diff |
annotate
|
| Thu, 01 Oct 2015 17:32:07 +0200 |
blanchet |
export '_cmd' functions
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:31 +0200 |
traytel |
more canonical context threading
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 18:36:16 +0200 |
blanchet |
made code less loopy
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 17:38:36 +0200 |
blanchet |
generalized generic translation function
|
file |
diff |
annotate
|
| Mon, 13 Jul 2015 19:22:55 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 21:59:16 +0200 |
blanchet |
tuned ML signature (and rationalized code a bit)
|
file |
diff |
annotate
|
| Tue, 07 Jul 2015 18:37:25 +0200 |
blanchet |
tuned ML signature
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 11:03:02 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 18:23:01 +0200 |
blanchet |
renamed ML funs
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 14:03:18 +0200 |
blanchet |
generalized code
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 18:46:16 +0200 |
blanchet |
tuned signature
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 17:24:55 +0200 |
blanchet |
generalized slightly
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 15:14:14 +0200 |
blanchet |
generalized code
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 15:14:12 +0200 |
blanchet |
generalized code
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 14:38:20 +0200 |
blanchet |
export ML function
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 19:17:41 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 23:39:42 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 18:36:29 +0100 |
wenzelm |
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 18:10:56 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 21:31:19 +0100 |
blanchet |
export more functions (for future 'corec')
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:53:16 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 09:49:16 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 16:45:24 +0100 |
blanchet |
avoid needless 'if ... undefined' in generated theorems
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 14:25:45 +0100 |
blanchet |
deal better with corecursion through functions
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:44:41 +0100 |
blanchet |
removed too strict checks
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 12:32:11 +0100 |
blanchet |
message tuning
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 12:19:05 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
improved primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
improved primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
better primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
more primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
more precise primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
more precise primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
better primcorec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
more 'primcorec' error handling
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
helpful error message when 'auto' fails
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
no quick_and_dirty for goals that may fail + tuned messages
|
file |
diff |
annotate
|