| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
a85372cb |
|
22-Dec-2016 |
blanchet <none@none> |
export ML function
|
| #
a972b36d |
|
20-Dec-2016 |
blanchet <none@none> |
generalized code (towards nonuniform datatypes)
|
| #
dff4c913 |
|
21-Dec-2016 |
blanchet <none@none> |
export ML function (towards nonuniform datatypes)
|
| #
b090623b |
|
21-Dec-2016 |
blanchet <none@none> |
renamed confusing variable names
|
| #
1df1830f |
|
27-Oct-2016 |
blanchet <none@none> |
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
|
| #
2c388eb7 |
|
06-Oct-2016 |
traytel <none@none> |
less aggressive unfolding in tactic
|
| #
3f54f2da |
|
12-Sep-2016 |
blanchet <none@none> |
strengthened tactic
|
| #
5f9ffa7e |
|
12-Sep-2016 |
blanchet <none@none> |
strengthened tactic
|
| #
bd27a761 |
|
12-Sep-2016 |
blanchet <none@none> |
prove 'set' property backward
|
| #
63fa20eb |
|
11-Sep-2016 |
blanchet <none@none> |
generalized code towards nonuniform (co)datatypes
|
| #
e3d144da |
|
11-Sep-2016 |
blanchet <none@none> |
strengthened tactics
|
| #
a1eb81ce |
|
11-Sep-2016 |
blanchet <none@none> |
derive relator properties forward
|
| #
257f9e69 |
|
11-Sep-2016 |
blanchet <none@none> |
derive maps forward
|
| #
0b1a60e0 |
|
11-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
cf6acf23 |
|
28-Apr-2016 |
wenzelm <none@none> |
unfold is subject to unfold_abs_def (still inactive);
tuned signature;
|
| #
7f231430 |
|
07-Mar-2016 |
blanchet <none@none> |
strengthened tactic
|
| #
97b25dd9 |
|
17-Feb-2016 |
blanchet <none@none> |
making 'pred_inject' a first-class BNF citizen
|
| #
591a7bfe |
|
01-Dec-2015 |
blanchet <none@none> |
tuned whitespace
|
| #
bcc1a605 |
|
06-Oct-2015 |
blanchet <none@none> |
generate 'case_transfer' unconditionally
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
93c132db |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
dbbe37ca |
|
15-Jul-2015 |
traytel <none@none> |
{r,e,d,f}tac with proper context in BNF
|
| #
1426640f |
|
30-Mar-2015 |
blanchet <none@none> |
export more low-level theorems in data structure (partly for 'corec')
|
| #
9113f38b |
|
24-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
2eeb52fe |
|
10-Mar-2015 |
blanchet <none@none> |
tuning
|
| #
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
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
935718a8 |
|
04-Jan-2015 |
blanchet <none@none> |
tuning
|
| #
e19d8ca4 |
|
19-Dec-2014 |
desharna <none@none> |
remove duplication in tactic
|
| #
765b19a0 |
|
10-Nov-2014 |
desharna <none@none> |
make 'corec_transfer' tactic more robust
|
| #
eb5e73fc |
|
11-Nov-2014 |
desharna <none@none> |
make 'rec_transfer' tactic more robust
|
| #
824744a2 |
|
21-Oct-2014 |
desharna <none@none> |
generate 'map_o_corec' for (co)datatypes
* * *
document 'map_o_corec'
|
| #
686351a9 |
|
21-Oct-2014 |
desharna <none@none> |
move theorem 'rec_o_map'
* * *
move documentation of 'rec_o_map'
|
| #
f05f85f5 |
|
14-Oct-2014 |
desharna <none@none> |
generate 'sel_transfer' for (co)datatypes
|
| #
cbfdc100 |
|
08-Oct-2014 |
wenzelm <none@none> |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
| #
5bbf7250 |
|
01-Oct-2014 |
blanchet <none@none> |
tuning
|
| #
069e3e8d |
|
26-Sep-2014 |
desharna <none@none> |
make 'case_transfer' tactic more robust
|
| #
eb1ed55c |
|
25-Sep-2014 |
desharna <none@none> |
generate 'corec_transfer' for codatatypes
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
8690a334 |
|
22-Sep-2014 |
desharna <none@none> |
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
|
| #
283614be |
|
17-Sep-2014 |
blanchet <none@none> |
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
|
| #
ffb23fae |
|
16-Sep-2014 |
blanchet <none@none> |
tuned fact visibility
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
| #
10742fde |
|
12-Sep-2014 |
desharna <none@none> |
make 'ctr_transfer' tactic more robust
|
| #
bbf13194 |
|
12-Sep-2014 |
desharna <none@none> |
make 'rel_sel' and 'map_sel' tactics more robust
|
| #
eeeb6513 |
|
04-Sep-2014 |
blanchet <none@none> |
renamed internal constant
|
| #
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
| #
2326a269 |
|
01-Sep-2014 |
blanchet <none@none> |
renamed BNF theories
--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy
|
| #
7666c0e4 |
|
29-Aug-2014 |
desharna <none@none> |
generate 'disc_transfer' for (co)datatypes
|
| #
dffb56b9 |
|
29-Aug-2014 |
desharna <none@none> |
generate 'case_transfer' for (co)datatypes
|
| #
c810fc8c |
|
27-Aug-2014 |
blanchet <none@none> |
removed not so interesting 'set_empty'
|
| #
64ca7457 |
|
21-Aug-2014 |
desharna <none@none> |
fix tactic failure with rel_induct0
minimal example:
datatype_new 'a A1 = A1 nat
and 'a A2 = A2 'a
|
| #
61a0a307 |
|
19-Aug-2014 |
desharna <none@none> |
generate 'ctr_transfer' for (co)datatypes
|
| #
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
| #
31574ff5 |
|
11-Aug-2014 |
desharna <none@none> |
generate 'set_cases' theorem for (co)datatypes
|
| #
534babeb |
|
11-Aug-2014 |
desharna <none@none> |
generate 'set_intros' theorem for (co)datatypes
|
| #
c96acc61 |
|
06-Aug-2014 |
blanchet <none@none> |
generate nicer 'set' theorems for (co)datatypes
|
| #
a1b49062 |
|
27-Jul-2014 |
desharna <none@none> |
made tactic more robust w.r.t. dead variables; tuned;
|
| #
e35b493c |
|
25-Jul-2014 |
blanchet <none@none> |
compile
|
| #
7b8e65c1 |
|
25-Jul-2014 |
blanchet <none@none> |
tuning
|
| #
0352f504 |
|
16-Jul-2014 |
desharna <none@none> |
generate 'rel_sel' theorem for (co)datatypes
|
| #
e1bd1185 |
|
16-Jul-2014 |
desharna <none@none> |
fix rel_cases
|
| #
3d51a59e |
|
14-Jul-2014 |
blanchet <none@none> |
took out 'rel_cases' for now because of failing tactic
|
| #
8ba9107a |
|
07-Jul-2014 |
desharna <none@none> |
refactor some tactics
|
| #
96d344e8 |
|
07-Jul-2014 |
desharna <none@none> |
refactor some tactics
|
| #
793f1234 |
|
07-Jul-2014 |
desharna <none@none> |
generate 'rel_cases' theorem for (co)datatypes
|
| #
c335096a |
|
01-Jul-2014 |
desharna <none@none> |
generate 'rel_induct' theorem for datatypes
|
| #
c1bd04e5 |
|
27-Jun-2014 |
blanchet <none@none> |
compile
|
| #
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'
|
| #
a0ad2713 |
|
24-Jun-2014 |
desharna <none@none> |
generate 'rel_coinduct0' theorem for codatatypes
|
| #
112d96ec |
|
02-Jun-2014 |
desharna <none@none> |
generate 'sel_set' theorem for (co)datatypes
|
| #
440f2078 |
|
21-May-2014 |
desharna <none@none> |
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
|
| #
d90e6fd8 |
|
15-May-2014 |
desharna <none@none> |
generate 'disc_map_iff[simp]' theorem for (co)datatypes
|
| #
360bae6b |
|
19-May-2014 |
desharna <none@none> |
fix 'set_empty' theorem when the discriminator is 'op ='
|
| #
09078cfa |
|
12-May-2014 |
desharna <none@none> |
generate 'set_empty' theorem for BNFs
|
| #
1c1981c6 |
|
27-Apr-2014 |
blanchet <none@none> |
cleaner 'rel_inject' theorems
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
d815b696 |
|
06-Mar-2014 |
blanchet <none@none> |
balance tuples that represent curried functions
|
| #
e1814034 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'prod_rel' to 'rel_prod'
|
| #
79f2884f |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'sum_rel' to 'rel_sum'
|
| #
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'
|
| #
53480a16 |
|
05-Mar-2014 |
traytel <none@none> |
more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
|
| #
367d5aaa |
|
04-Mar-2014 |
blanchet <none@none> |
simplify sets in BNF composition
|
| #
81595aad |
|
02-Mar-2014 |
blanchet <none@none> |
removed obsolete, harmful step in tactic
|
| #
a350d601 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
| #
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
| #
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
e3355c3e |
|
20-Jan-2014 |
blanchet <none@none> |
move BNF_LFP up the dependency chain
|
| #
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
|