| Wed, 28 Dec 2016 17:22:16 +0100 |
blanchet |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| 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
|