| 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
|
| 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
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
tuned new primrec messages
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:57:34 +0100 |
blanchet |
reworked primcorec error messages
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 21:24:14 +0100 |
blanchet |
generate [code] only with 'code' plugin enabled
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 10:09:42 +0100 |
blanchet |
added plugins syntax to prim(co)rec
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 09:54:41 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 14:06:13 +0100 |
desharna |
Add plugin to generate transfer theorem for primrec and primcorec
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
keep all 'ctr' theorems
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
smoothly handle unit codatatypes in 'primcorec'
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
careful with de Bruijn indices
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:28 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 13:41:40 +0200 |
blanchet |
more honest 'primcorec' -- don't parse a theorem name that is then ignored
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 13:38:21 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 13:27:04 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:40 +0200 |
blanchet |
export useful functions for users of (co)recursors
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:28:00 +0200 |
blanchet |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
less aggressive unfolding; removed debugging;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2014 01:59:23 +0200 |
panny |
fix typo
|
file |
diff |
annotate
|
| Mon, 14 Jul 2014 01:35:43 +0200 |
panny |
throw error for bad input
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
add helper function map_prod
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
| Tue, 13 May 2014 11:10:22 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 05 May 2014 09:30:20 +0200 |
blanchet |
simplify selectors in code views
|
file |
diff |
annotate
|
| Thu, 01 May 2014 14:07:27 +0200 |
panny |
use qualified name (was interpreted as a catch-all variable name)
|
file |
diff |
annotate
|
| Thu, 01 May 2014 14:05:29 +0200 |
panny |
add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 01:36:38 +0100 |
panny |
add error messages for invalid inputs
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
use balanced tuples in 'primcorec'
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 01:02:21 +0100 |
blanchet |
balance tuples that represent curried functions
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed (co)iterators from documentation
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
avoid duplicate 'disc_iff' theorems
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'diff_iff' a simp rule if available
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
less aggressive resolving
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 13:04:57 +0100 |
blanchet |
correct most general type for mutual recursion when several identical types are involved
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:08:59 +0100 |
blanchet |
prepare two-stage 'primrec' setup
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:54:38 +0100 |
blanchet |
simplified data structure by reducing the incidence of clumsy indices
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 18:18:27 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
tuning: moved code where it belongs
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:41 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|