| Fri, 23 Dec 2016 00:13:30 +0100 |
blanchet |
generalized generation of coinduction goal (towards nonuniform codatatypes)
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 19:14:58 +0100 |
blanchet |
export ML functions (towards nonuniform codatatypes) + signature tuning
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 11:45:16 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 11:14:37 +0100 |
blanchet |
renamed confusing variable names
|
file |
diff |
annotate
|
| Tue, 20 Dec 2016 16:17:13 +0100 |
blanchet |
generalized code (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Fri, 16 Dec 2016 22:54:14 +0100 |
blanchet |
refactored induction principle generation code, for reuse for nonuniform datatypes
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 14:14:58 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 14:14:48 +0200 |
blanchet |
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
|
file |
diff |
annotate
|
| Wed, 26 Oct 2016 22:40:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 06 Oct 2016 13:33:26 +0200 |
traytel |
less aggressive unfolding in tactic
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 16:23:12 +0200 |
blanchet |
union associates to the left
|
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
|
| Mon, 12 Sep 2016 16:51:55 +0200 |
blanchet |
avoid warning triggered by code generator
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 13:35:29 +0200 |
blanchet |
prove 'set' property backward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 23:32:45 +0200 |
blanchet |
generalized code towards nonuniform (co)datatypes
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 15:37:09 +0200 |
blanchet |
strengthened tactics
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
derive relator properties forward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
derive maps forward
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 13:35:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:35:08 +0200 |
blanchet |
made it easier to catch 'empty datatype' exception
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:39 +0200 |
blanchet |
export ML functions
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 16:06:59 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
exported ML functions + tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 13:53:16 +0200 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 15:23:01 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 15:04:02 +0200 |
blanchet |
generalized ML signature
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 10:09:33 +0200 |
blanchet |
tuned ML signature
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 20:57:07 +0200 |
blanchet |
exported ML functions
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 18:40:29 +0200 |
blanchet |
export ML function + tuning
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 13:09:18 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 11:35:42 +0200 |
blanchet |
export more ML functions
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
tuned ML
|
file |
diff |
annotate
|
| Tue, 26 Jul 2016 14:29:20 +0200 |
traytel |
honor sorts in (co)datatype declarations
|
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, 25 Apr 2016 21:09:02 +0200 |
blanchet |
avoid duplicate mixfix messages in '(co)datatype' type name
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML interface
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 07:57:02 +0100 |
blanchet |
better warning, with definitions in right order
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 19:05:18 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:50:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:50:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:08:36 +0100 |
blanchet |
making 'pred_inject' a first-class BNF citizen
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 18:27:17 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 13:30:04 +0100 |
blanchet |
keep 'ctor_iff_dtor' theorem around in BNF FP database
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:48:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 09:09:37 +0100 |
blanchet |
generate stronger 'rel_(co)induct' and 'coinduct' principles for mutually (co)recursive (co)datatypes
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:58:38 +0100 |
blanchet |
don't pollute local theory with needless names
|
file |
diff |
annotate
|
| Thu, 08 Oct 2015 22:41:21 +0200 |
blanchet |
tuning
|
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 21:04:44 +0200 |
blanchet |
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 18:39:31 +0200 |
blanchet |
generate 'case_transfer' unconditionally
|
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
|
| Wed, 23 Sep 2015 09:50:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:32:23 +0200 |
wenzelm |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 21:40:59 +0200 |
wenzelm |
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 17:25:48 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 22:56:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 07 Apr 2015 17:24:55 +0200 |
blanchet |
generalized slightly
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 15:29:09 +0200 |
wenzelm |
more standard Long_Name operations;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2015 17:10:24 +0100 |
blanchet |
store low-level (un)fold constants
|
file |
diff |
annotate
|
| Thu, 26 Mar 2015 16:42:42 +0100 |
blanchet |
export more functions
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 18:10:56 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
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 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
|
| Tue, 11 Nov 2014 12:30:36 +0100 |
desharna |
also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 10:26:08 +0100 |
desharna |
make 'rec_transfer' tactic more robust
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 20:43:13 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:21:59 +0100 |
desharna |
fix 'unfla' function
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
generate 'map_o_corec' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:10 +0200 |
desharna |
warn for not fully mutually (co)recursive types
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 11:56:46 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:36 +0200 |
desharna |
generate 'sel_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:34 +0200 |
desharna |
add 'kind' to 'cr_sugar'
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:57 +0200 |
desharna |
add 'fp_bnf' to 'bnf_sugar'
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:56 +0200 |
desharna |
preserve the structure of 'set_intros' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:54 +0200 |
desharna |
preserve the structure of 'map_sel' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:11:35 +0200 |
desharna |
preserve the structure of 'set_sel' theorem in ML
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
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
|
| Mon, 06 Oct 2014 13:42:48 +0200 |
desharna |
refactor 'map_sel_thms' and 'set_sel_thms'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:41:37 +0200 |
desharna |
rename 'xtor_rel_thms' to 'xtor_rels'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:56 +0200 |
desharna |
rename 'xtor_set_thmss' to 'xtor_setss'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:31 +0200 |
desharna |
rename 'xtor_map_thms' to 'xtor_maps'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:02 +0200 |
desharna |
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:39:12 +0200 |
desharna |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:40 +0200 |
desharna |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:13 +0200 |
desharna |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:48 +0200 |
desharna |
add 'set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:47 +0200 |
desharna |
add 'common_set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:42 +0200 |
desharna |
add 'rel_co_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:29 +0200 |
desharna |
add 'common_rel_co_induct' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:15 +0200 |
desharna |
add 'co_rec_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:03 +0200 |
desharna |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:49 +0200 |
desharna |
add 'disc_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|