| #
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
|
| #
c923351f |
|
17-Jun-2016 |
blanchet <none@none> |
killed dead code
|
| #
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
|
| #
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;
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
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
|
| #
9ec94e1d |
|
23-Sep-2015 |
traytel <none@none> |
congruence rules for the relator
|
| #
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
|
| #
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
|
| #
8a20662e |
|
25-Sep-2014 |
desharna <none@none> |
generate 'dtor_corec_transfer' for codatatypes
|
| #
3b70a467 |
|
09-Sep-2014 |
blanchet <none@none> |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
| #
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
|
| #
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
|
| #
d67d21fb |
|
26-May-2014 |
blanchet <none@none> |
don't conceal (co)datatypes
|
| #
f5f7066b |
|
27-Apr-2014 |
blanchet <none@none> |
more reliable 'name_of_bnf'
|
| #
91b99046 |
|
10-Apr-2014 |
traytel <none@none> |
more accurate type arguments for intermeadiate typedefs
|
| #
a5ed49ac |
|
01-Apr-2014 |
blanchet <none@none> |
tuning
|
| #
cb2fcf0f |
|
01-Apr-2014 |
blanchet <none@none> |
added BNF interpretation hook
|
| #
04333f87 |
|
25-Mar-2014 |
traytel <none@none> |
prove theorems with fixed variables (export afterwards)
|
| #
b7ad1ed8 |
|
17-Mar-2014 |
traytel <none@none> |
tuned internal construction
|
| #
e547e99a |
|
13-Mar-2014 |
traytel <none@none> |
tuned tactics
|
| #
7e406702 |
|
13-Mar-2014 |
traytel <none@none> |
simplified internal codatatype construction
|
| #
c636cfec |
|
10-Mar-2014 |
traytel <none@none> |
tuned tactic
|
| #
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;
|
| #
59071525 |
|
04-Mar-2014 |
blanchet <none@none> |
removed debugging leftover
|
| #
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
|
| #
9b4e4d1a |
|
20-Feb-2014 |
traytel <none@none> |
only one internal coinduction rule
|
| #
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
| #
f8b6d8a9 |
|
20-Feb-2014 |
traytel <none@none> |
made tactics more robust
|
| #
cef07af3 |
|
18-Feb-2014 |
traytel <none@none> |
another simplification of internal codatatype construction
|
| #
47479eff |
|
19-Feb-2014 |
traytel <none@none> |
simplifications of internal codatatype construction
|
| #
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)
|
| #
34a0be19 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'
|
| #
40e0ba91 |
|
12-Feb-2014 |
blanchet <none@none> |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
a6c1110f |
|
12-Feb-2014 |
blanchet <none@none> |
adapted theories to '{case,rec}_{list,option}' names
|
| #
4fc86ba9 |
|
12-Feb-2014 |
blanchet <none@none> |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
* * *
cleaner simp/iff sets
|
| #
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
|
| #
b575b3f0 |
|
20-Jan-2014 |
blanchet <none@none> |
made BNF compile after move to HOL
|
| #
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
|