| #
31acc623 |
|
06-Dec-2019 |
wenzelm <none@none> |
clarified modules;
|
| #
e2750756 |
|
06-Dec-2019 |
wenzelm <none@none> |
misc tuning and clarification: proper check of datatype kind;
|
| #
3c2f0722 |
|
06-Dec-2019 |
wenzelm <none@none> |
clarified modules;
|
| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
0ed93039 |
|
04-Jan-2019 |
wenzelm <none@none> |
support for isabelle update -u control_cartouches;
|
| #
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
| #
82b44857 |
|
25-Jan-2018 |
wenzelm <none@none> |
clarified signature: items with \isasep are special;
|
| #
0bcb05ae |
|
18-Jan-2018 |
wenzelm <none@none> |
clarified access to antiquotation options;
define explicit variants of antiquotations;
output proper Latex.text;
misc tuning and clarification;
|
| #
0ce84d08 |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified modules;
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
8aafd76b |
|
26-Oct-2016 |
blanchet <none@none> |
tuning
|
| #
bd27a761 |
|
12-Sep-2016 |
blanchet <none@none> |
prove 'set' property backward
|
| #
36e94838 |
|
11-Sep-2016 |
blanchet <none@none> |
provide a mechanism for ensuring dead type variables occur in typedef if desired
|
| #
14393da9 |
|
08-Sep-2016 |
blanchet <none@none> |
made it easier to catch 'empty datatype' exception
|
| #
dc32db36 |
|
07-Sep-2016 |
blanchet <none@none> |
tuned whitespace
|
| #
28ad8145 |
|
06-Sep-2016 |
blanchet <none@none> |
generalized ML signature
|
| #
68b4ac3c |
|
06-Sep-2016 |
blanchet <none@none> |
generalized code (subtly)
|
| #
25f52df5 |
|
06-Sep-2016 |
blanchet <none@none> |
tuned ML signature
|
| #
3d9861ee |
|
05-Sep-2016 |
blanchet <none@none> |
export ML function + tuning
|
| #
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
|
| #
5c914c99 |
|
03-Apr-2016 |
traytel <none@none> |
tuned names
|
| #
c4b0715f |
|
27-Mar-2016 |
blanchet <none@none> |
generalized ML function
|
| #
4dd3178f |
|
27-Mar-2016 |
blanchet <none@none> |
added '_legacy' suffixes
|
| #
204828b6 |
|
27-Mar-2016 |
blanchet <none@none> |
generalized ML interface
|
| #
40b7f6c2 |
|
22-Mar-2016 |
blanchet <none@none> |
added timers to N2M
|
| #
830f4f54 |
|
22-Mar-2016 |
traytel <none@none> |
document that n2m does not depend on most things in fp_sugar in its type
|
| #
e786a3b5 |
|
14-Mar-2016 |
blanchet <none@none> |
generalized ML function
|
| #
97b25dd9 |
|
17-Feb-2016 |
blanchet <none@none> |
making 'pred_inject' a first-class BNF citizen
|
| #
7cff5a9a |
|
11-Jan-2016 |
blanchet <none@none> |
tuning
|
| #
2678006a |
|
11-Jan-2016 |
blanchet <none@none> |
exported ML function
|
| #
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
46ef1e1e |
|
16-Jul-2015 |
blanchet <none@none> |
tuning
|
| #
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
| #
0e2b1250 |
|
01-Apr-2015 |
blanchet <none@none> |
simplified code
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
5b8baa9f |
|
30-Mar-2015 |
wenzelm <none@none> |
support for strictly private name space entries;
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
|
| #
2eeb52fe |
|
10-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
65c57129 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
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};
|
| #
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
|
| #
8a20662e |
|
25-Sep-2014 |
desharna <none@none> |
generate 'dtor_corec_transfer' for codatatypes
|
| #
fce1041d |
|
25-Sep-2014 |
desharna <none@none> |
generate 'ctor_rec_transfer' for datatypes
|
| #
22f3dd87 |
|
13-Sep-2014 |
blanchet <none@none> |
imported patch phantoms
|
| #
abf5628f |
|
09-Sep-2014 |
blanchet <none@none> |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
| #
3b70a467 |
|
09-Sep-2014 |
blanchet <none@none> |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
| #
241c5b8f |
|
08-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
f4f86474 |
|
04-Sep-2014 |
blanchet <none@none> |
moved code around
|
| #
0a4b950c |
|
02-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
9c861e3b |
|
01-Sep-2014 |
blanchet <none@none> |
more compatibility between old- and new-style datatypes
|
| #
978db45e |
|
01-Sep-2014 |
blanchet <none@none> |
made transfer functions slightly more general
|
| #
01e96211 |
|
01-Sep-2014 |
traytel <none@none> |
goal generation for xtor_co_rec_transfer
|
| #
ecce9362 |
|
25-Sep-2014 |
traytel <none@none> |
even more deads go to the end (continuation of e3a01b73579f)
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
7b8e65c1 |
|
25-Jul-2014 |
blanchet <none@none> |
tuning
|
| #
0352f504 |
|
16-Jul-2014 |
desharna <none@none> |
generate 'rel_sel' theorem for (co)datatypes
|
| #
8ba9107a |
|
07-Jul-2014 |
desharna <none@none> |
refactor some tactics
|
| #
793f1234 |
|
07-Jul-2014 |
desharna <none@none> |
generate 'rel_cases' theorem for (co)datatypes
|
| #
109d7354 |
|
03-Jul-2014 |
desharna <none@none> |
generate 'rel_intros' theorem for (co)datatypes
|
| #
34b0a47c |
|
02-Jul-2014 |
desharna <none@none> |
generate 'corec_code' theorem for codatatypes
|
| #
6f5ea271 |
|
27-Jun-2014 |
blanchet <none@none> |
tuned variable names
|
| #
7bbce892 |
|
30-Jul-2014 |
desharna <none@none> |
generate 'set_induct' theorem for codatatypes
|
| #
ebf08b80 |
|
23-Apr-2014 |
blanchet <none@none> |
no need to make 'size' generation an interpretation -- overkill
|
| #
7e406702 |
|
13-Mar-2014 |
traytel <none@none> |
simplified internal codatatype construction
|
| #
da328fb3 |
|
07-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
| #
c4dc0538 |
|
07-Mar-2014 |
blanchet <none@none> |
use balanced tuples in 'primcorec'
|
| #
147d4ad6 |
|
07-Mar-2014 |
blanchet <none@none> |
tuning
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
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'
|
| #
337aab8e |
|
04-Mar-2014 |
blanchet <none@none> |
more caching in composition pipeline
|
| #
908441e2 |
|
04-Mar-2014 |
blanchet <none@none> |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
| #
095de857 |
|
03-Mar-2014 |
traytel <none@none> |
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
|
| #
c39b02f9 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
5f1d2990 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
a3a1f899 |
|
02-Mar-2014 |
blanchet <none@none> |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
| #
94bfc55c |
|
02-Mar-2014 |
blanchet <none@none> |
optimize cardinal bounds involving natLeq (omega)
|
| #
bbeeaf3d |
|
28-Feb-2014 |
traytel <none@none> |
load Metis a little later
|
| #
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
| #
70ca7611 |
|
23-Feb-2014 |
blanchet <none@none> |
added BNF cache (within one definition)
|
| #
b7af0cc0 |
|
23-Feb-2014 |
blanchet <none@none> |
optimization of 'bnf_of_typ' if all variables are dead
|
| #
2f1f0a53 |
|
23-Feb-2014 |
blanchet <none@none> |
added explicit killing
|
| #
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
| #
04523a1c |
|
19-Feb-2014 |
blanchet <none@none> |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
| #
e9c8b8d7 |
|
18-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
2f309df2 |
|
14-Feb-2014 |
blanchet <none@none> |
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
|
| #
2a0c4d96 |
|
14-Feb-2014 |
blanchet <none@none> |
better handling of recursion through functions
|
| #
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
|