#
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;
|
#
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
#
038835b6 |
|
11-Jan-2018 |
wenzelm <none@none> |
uniform use of Standard ML op-infix -- eliminated warnings;
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
8aafd76b |
|
26-Oct-2016 |
blanchet <none@none> |
tuning
|
#
14393da9 |
|
08-Sep-2016 |
blanchet <none@none> |
made it easier to catch 'empty datatype' exception
|
#
920ec25c |
|
17-Jun-2016 |
blanchet <none@none> |
killed deadcode
|
#
237f0cff |
|
02-Jun-2016 |
wenzelm <none@none> |
eliminated pointless alias (no warning for duplicates);
|
#
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
|
#
4dd3178f |
|
27-Mar-2016 |
blanchet <none@none> |
added '_legacy' suffixes
|
#
fe42a4e9 |
|
22-Mar-2016 |
blanchet <none@none> |
tuned whitespace
|
#
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
|
#
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
e5517855 |
|
05-Oct-2015 |
traytel <none@none> |
collect the names from goals in favor of fragile exports
|
#
b8e4db45 |
|
25-Sep-2015 |
traytel <none@none> |
restructure fresh variable generation to make exports more wellformed
|
#
2813b7ac |
|
25-Sep-2015 |
traytel <none@none> |
more canonical context threading
|
#
78d8b09f |
|
03-Sep-2015 |
traytel <none@none> |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
839d9ae3 |
|
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
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
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
|
#
9113f38b |
|
24-Mar-2015 |
blanchet <none@none> |
tuning
|
#
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
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
9e653fc8 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper proof context for typedef;
|
#
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
|
#
fce1041d |
|
25-Sep-2014 |
desharna <none@none> |
generate 'ctor_rec_transfer' for datatypes
|
#
22f3dd87 |
|
13-Sep-2014 |
blanchet <none@none> |
imported patch phantoms
|
#
4264224c |
|
11-Sep-2014 |
blanchet <none@none> |
tuning terminology
|
#
823ba92f |
|
11-Sep-2014 |
blanchet <none@none> |
compile
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
#
3b70a467 |
|
09-Sep-2014 |
blanchet <none@none> |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
#
02b89845 |
|
08-Sep-2014 |
blanchet <none@none> |
tuned command descriptions
|
#
35dc0252 |
|
08-Sep-2014 |
blanchet <none@none> |
generate better internal names, with name of the target type in it
|
#
241c5b8f |
|
08-Sep-2014 |
blanchet <none@none> |
tuning
|
#
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
#
3a5bbb8e |
|
03-Sep-2014 |
blanchet <none@none> |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
#
01e96211 |
|
01-Sep-2014 |
traytel <none@none> |
goal generation for xtor_co_rec_transfer
|
#
57efbcf6 |
|
19-Aug-2014 |
blanchet <none@none> |
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
|
#
6078680b |
|
18-Aug-2014 |
desharna <none@none> |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
#
173fde0a |
|
14-Aug-2014 |
desharna <none@none> |
generate 'rel_map' theorem for BNFs
|
#
97fe0137 |
|
23-Jul-2014 |
blanchet <none@none> |
use the noted theorem whenever possible, also in 'BNF_Def'
|
#
efd75a1e |
|
17-Jul-2014 |
desharna <none@none> |
add mk_Trueprop_mem utility function
|
#
d220e20b |
|
31-Jul-2014 |
traytel <none@none> |
simplified tactics slightly
|
#
7bbce892 |
|
30-Jul-2014 |
desharna <none@none> |
generate 'set_induct' theorem for codatatypes
|
#
bd75d378 |
|
24-Jun-2014 |
blanchet <none@none> |
tuning
|
#
d67d21fb |
|
26-May-2014 |
blanchet <none@none> |
don't conceal (co)datatypes
|
#
f5f7066b |
|
27-Apr-2014 |
blanchet <none@none> |
more reliable 'name_of_bnf'
|
#
aea2cf85 |
|
23-Apr-2014 |
blanchet <none@none> |
localize new size function generation code
|
#
df15a7e7 |
|
23-Apr-2014 |
blanchet <none@none> |
generate size instances for new-style datatypes
|
#
91b99046 |
|
10-Apr-2014 |
traytel <none@none> |
more accurate type arguments for intermeadiate typedefs
|
#
c41b7bfc |
|
01-Apr-2014 |
traytel <none@none> |
more precise BNF bound for datatypes
|
#
a5ed49ac |
|
01-Apr-2014 |
blanchet <none@none> |
tuning
|
#
cb2fcf0f |
|
01-Apr-2014 |
blanchet <none@none> |
added BNF interpretation hook
|
#
1c38bdbc |
|
01-Apr-2014 |
traytel <none@none> |
tuned
|
#
04333f87 |
|
25-Mar-2014 |
traytel <none@none> |
prove theorems with fixed variables (export afterwards)
|
#
f626d9cf |
|
24-Mar-2014 |
traytel <none@none> |
made tactic more robust
|
#
e4e91ca5 |
|
21-Mar-2014 |
traytel <none@none> |
simplified internal datatype construction
|
#
f826f38d |
|
18-Mar-2014 |
traytel <none@none> |
changed policy when to define constants
|
#
e547e99a |
|
13-Mar-2014 |
traytel <none@none> |
tuned tactics
|
#
0bd56fcf |
|
10-Mar-2014 |
traytel <none@none> |
unfold intermediate definitions after sealing the bnf
|
#
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;
|
#
5f1d2990 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
#
94bfc55c |
|
02-Mar-2014 |
blanchet <none@none> |
optimize cardinal bounds involving natLeq (omega)
|
#
dd1a06aa |
|
25-Feb-2014 |
traytel <none@none> |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
#
a6bc1928 |
|
26-Feb-2014 |
traytel <none@none> |
intermediate typedef for the type of the bound (local to lfp)
|
#
87bc9273 |
|
26-Feb-2014 |
traytel <none@none> |
made tactics more robust
|
#
cab04828 |
|
23-Feb-2014 |
blanchet <none@none> |
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
|
#
3899b695 |
|
18-Feb-2014 |
traytel <none@none> |
syntactic simplifications of internal (co)datatype constructions
|
#
a4bafeb9 |
|
17-Feb-2014 |
blanchet <none@none> |
tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'
|
#
0837409d |
|
17-Feb-2014 |
blanchet <none@none> |
tuning: moved code where it belongs
|
#
7159fe0c |
|
14-Feb-2014 |
traytel <none@none> |
register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
|
#
136b070b |
|
30-Jan-2014 |
traytel <none@none> |
use Local_Theory.define instead of Specification.definition for internal constants
|
#
376fc3bb |
|
31-Jan-2014 |
traytel <none@none> |
less hermetic tactics
|
#
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
|