| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
c5769784 |
|
02-Jan-2018 |
blanchet <none@none> |
avoid call to function that may throw an exception in error message
|
| #
502ab55a |
|
30-Dec-2016 |
blanchet <none@none> |
more uniform errors in '(prim)(co)rec(ursive)' variants
|
| #
bb1d3a61 |
|
28-Dec-2016 |
blanchet <none@none> |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
| #
5851429c |
|
22-Mar-2016 |
blanchet <none@none> |
better warning, with definitions in right order
|
| #
8b456ccd |
|
05-Mar-2015 |
blanchet <none@none> |
tuned new primrec messages
|
| #
7137e328 |
|
07-Jan-2015 |
blanchet <none@none> |
made SML/NJ happier
|
| #
1de6462a |
|
05-Jan-2015 |
blanchet <none@none> |
added plugins syntax to prim(co)rec
|
| #
07a7056b |
|
19-Dec-2014 |
desharna <none@none> |
Add plugin to generate transfer theorem for primrec and primcorec
|
| #
2a9622ce |
|
15-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
75fd5395 |
|
08-Sep-2014 |
blanchet <none@none> |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
| #
aea2cf85 |
|
23-Apr-2014 |
blanchet <none@none> |
localize new size function generation code
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
c39b02f9 |
|
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)
|
| #
ae64540a |
|
27-Feb-2014 |
blanchet <none@none> |
correct most general type for mutual recursion when several identical types are involved
|
| #
04523a1c |
|
19-Feb-2014 |
blanchet <none@none> |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
| #
1770bd13 |
|
19-Feb-2014 |
blanchet <none@none> |
tuning
|
| #
efebaf05 |
|
18-Feb-2014 |
blanchet <none@none> |
prepare two-stage 'primrec' setup
|
| #
2a0c4d96 |
|
14-Feb-2014 |
blanchet <none@none> |
better handling of recursion through functions
|
| #
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
|