| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
8aafd76b |
|
26-Oct-2016 |
blanchet <none@none> |
tuning
|
| #
dc32db36 |
|
07-Sep-2016 |
blanchet <none@none> |
tuned whitespace
|
| #
ede74783 |
|
15-Apr-2016 |
traytel <none@none> |
intermediate definitions and caching in n2m to keep terms small
|
| #
057633fe |
|
14-Apr-2016 |
traytel <none@none> |
n2m operates on (un)folds
|
| #
049cf95c |
|
07-Apr-2016 |
traytel <none@none> |
(un)folds are not legacy
|
| #
0ec920ec |
|
07-Apr-2016 |
traytel <none@none> |
derive (co)rec uniformly from (un)fold
|
| #
1a96a7b9 |
|
05-Apr-2016 |
traytel <none@none> |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
| #
4dd3178f |
|
27-Mar-2016 |
blanchet <none@none> |
added '_legacy' suffixes
|
| #
e449dcd3 |
|
27-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
15a49b89 |
|
22-Mar-2016 |
blanchet <none@none> |
more debugging
|
| #
830f4f54 |
|
22-Mar-2016 |
traytel <none@none> |
document that n2m does not depend on most things in fp_sugar in its type
|
| #
d6329198 |
|
18-Mar-2016 |
traytel <none@none> |
normalize schematic names since they are used to instantiate the theorem later
|
| #
78d8b09f |
|
03-Sep-2015 |
traytel <none@none> |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
| #
a758d65a |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
1426640f |
|
30-Mar-2015 |
blanchet <none@none> |
export more low-level theorems in data structure (partly for 'corec')
|
| #
955d0fc8 |
|
26-Mar-2015 |
blanchet <none@none> |
store low-level (un)fold constants
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
95b46393 |
|
24-Nov-2014 |
traytel <none@none> |
preinstantiate (co)inductions in N2M to handle mutual but separated SCCs
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
9622cd51 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_rel_thms' to 'xtor_rels'
|
| #
191e6485 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_set_thmss' to 'xtor_setss'
|
| #
7d5fbd1c |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_map_thms' to 'xtor_maps'
|
| #
57c1cff0 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
| #
c54f4f14 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
| #
9665b67b |
|
06-Oct-2014 |
desharna <none@none> |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
| #
73c7c1b9 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
| #
eb1ed55c |
|
25-Sep-2014 |
desharna <none@none> |
generate 'corec_transfer' for codatatypes
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
bef0d212 |
|
18-Sep-2014 |
blanchet <none@none> |
careful with op = in n2m (actually by Dmitriy Traytel)
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
| #
41af0ef0 |
|
14-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
be1ca862 |
|
08-Sep-2014 |
traytel <none@none> |
made tactic more robust w.r.t. dead variables
|
| #
f4f86474 |
|
04-Sep-2014 |
blanchet <none@none> |
moved code around
|
| #
34bdceb0 |
|
02-Sep-2014 |
traytel <none@none> |
lessen the burden on the caller: sort where necessary in n2m
|
| #
b83b3935 |
|
06-Aug-2014 |
traytel <none@none> |
handle deep nesting in N2M
|
| #
3ea75498 |
|
06-Aug-2014 |
traytel <none@none> |
made tactic more robust
|
| #
52e1ed24 |
|
07-Jul-2014 |
desharna <none@none> |
add helper function map_prod
|
| #
6f5ea271 |
|
27-Jun-2014 |
blanchet <none@none> |
tuned variable names
|
| #
7bbce892 |
|
30-Jul-2014 |
desharna <none@none> |
generate 'set_induct' theorem for codatatypes
|
| #
020ff44f |
|
24-Jun-2014 |
desharna <none@none> |
tune the implementation of 'rel_coinduct'
|
| #
ebf08b80 |
|
23-Apr-2014 |
blanchet <none@none> |
no need to make 'size' generation an interpretation -- overkill
|
| #
72596a3c |
|
23-Apr-2014 |
blanchet <none@none> |
generate 'rec_o_map' and 'size_o_map' in size extension
|
| #
df15a7e7 |
|
23-Apr-2014 |
blanchet <none@none> |
generate size instances for new-style datatypes
|
| #
e95a570c |
|
10-Apr-2014 |
traytel <none@none> |
use mutual clique information (cf. c451cf8b29c8) to make N2M more robust
|
| #
4f878182 |
|
10-Apr-2014 |
traytel <none@none> |
made N2M tactic more robust
|
| #
6d54f022 |
|
09-Apr-2014 |
blanchet <none@none> |
thread mutual cliques through
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
8f53ef93 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_pair' to 'map_prod'
|
| #
433b1b70 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_sum' to 'sum_map'
|
| #
095de857 |
|
03-Mar-2014 |
traytel <none@none> |
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
|
| #
6ff5e9d6 |
|
03-Mar-2014 |
blanchet <none@none> |
simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
|
| #
5f1d2990 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
85e54101 |
|
02-Mar-2014 |
blanchet <none@none> |
make 'typedef' optional, depending on size of original type
|
| #
3553b2e2 |
|
01-Mar-2014 |
traytel <none@none> |
made SML/NJ happier
|
| #
85543ad0 |
|
28-Feb-2014 |
traytel <none@none> |
made SML/NJ happier
|
| #
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
| #
04523a1c |
|
19-Feb-2014 |
blanchet <none@none> |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
| #
af307af1 |
|
18-Feb-2014 |
blanchet <none@none> |
made SML/NJ happier
|
| #
8d680255 |
|
17-Feb-2014 |
blanchet <none@none> |
simplified data structure by reducing the incidence of clumsy indices
|
| #
a1d385ea |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'datatype_new_compat' to 'datatype_compat'
|
| #
44342b4b |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
|
| #
8d2e007d |
|
14-Feb-2014 |
traytel <none@none> |
made N2M more robust w.r.t. identical nested types
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
34f4cd23 |
|
12-Feb-2014 |
blanchet <none@none> |
more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's
|
| #
88a2727e |
|
20-Jan-2014 |
blanchet <none@none> |
tuned names
|
| #
e8e169dd |
|
20-Jan-2014 |
blanchet <none@none> |
adjusted comments
|
| #
a0868967 |
|
20-Jan-2014 |
blanchet <none@none> |
avoid nested 'Tools' directories
--HG--
rename : src/HOL/Tools/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/bnf_comp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/bnf_comp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/bnf_def.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/bnf_def_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/bnf_fp_n2m.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/bnf_fp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/bnf_gfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/bnf_gfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/bnf_lfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/bnf_lfp_compat.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/bnf_lfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/bnf_lfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/bnf_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/bnf_util.ML
|