| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
1a195bfa |
|
26-Jun-2017 |
blanchet <none@none> |
more error checking
|
| #
9147221e |
|
10-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
21083057 |
|
18-Aug-2016 |
traytel <none@none> |
derive pred_mono property for BNFs
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
040047c7 |
|
17-Feb-2016 |
traytel <none@none> |
derive transfer rule for predicator
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
2ceb4cc9 |
|
14-Nov-2015 |
wenzelm <none@none> |
option "inductive_defs" controls exposure of def and mono facts;
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
52852be3 |
|
13-Oct-2015 |
haftmann <none@none> |
emphasized general nature of parameter
|
| #
d180dd22 |
|
13-Oct-2015 |
haftmann <none@none> |
moved lemmas
|
| #
3349054e |
|
23-Sep-2015 |
traytel <none@none> |
more useful properties of the relators
|
| #
df44ab4c |
|
27-Aug-2015 |
haftmann <none@none> |
standardized some occurences of ancient "split" alias
--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
99c387f7 |
|
16-Mar-2015 |
traytel <none@none> |
BNF relators preserve reflexivity
|
| #
b7e3427a |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add monotonicity lemmas for rel_fun
|
| #
23571538 |
|
07-Nov-2014 |
traytel <none@none> |
more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
| #
0641da82 |
|
01-Sep-2014 |
desharna <none@none> |
generate 'set_transfer' for BNFs
|
| #
439a0059 |
|
01-Sep-2014 |
desharna <none@none> |
generate 'rel_transfer' for BNFs
|
| #
b83b3935 |
|
06-Aug-2014 |
traytel <none@none> |
handle deep nesting in N2M
|
| #
89c180c6 |
|
24-Jul-2014 |
wenzelm <none@none> |
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
|
| #
3816e708 |
|
27-Jun-2014 |
blanchet <none@none> |
merged two small theory files
|
| #
7cc5fea9 |
|
29-Jul-2014 |
blanchet <none@none> |
header tuning
|
| #
939a8149 |
|
23-Apr-2014 |
blanchet <none@none> |
added 'inj_map' as auxiliary BNF theorem
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
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
|
| #
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_...'
|
| #
1a605a5d |
|
29-Jan-2014 |
traytel <none@none> |
made tactic more robust
|
| #
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|
| #
9e021ec0 |
|
20-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
b575b3f0 |
|
20-Jan-2014 |
blanchet <none@none> |
made BNF compile after move to HOL
|
| #
5fd16e81 |
|
20-Jan-2014 |
blanchet <none@none> |
tuned comments
|
| #
28d1215f |
|
20-Jan-2014 |
blanchet <none@none> |
moved BNF files to 'HOL'
--HG--
rename : src/HOL/BNF/BNF_Comp.thy => src/HOL/BNF_Comp.thy
rename : src/HOL/BNF/BNF_Def.thy => src/HOL/BNF_Def.thy
rename : src/HOL/BNF/BNF_FP_Base.thy => src/HOL/BNF_FP_Base.thy
rename : src/HOL/BNF/BNF_GFP.thy => src/HOL/BNF_GFP.thy
rename : src/HOL/BNF/BNF_LFP.thy => src/HOL/BNF_LFP.thy
rename : src/HOL/BNF/BNF_Util.thy => src/HOL/BNF_Util.thy
rename : src/HOL/BNF/Basic_BNFs.thy => src/HOL/Basic_BNFs.thy
rename : src/HOL/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/Tools/bnf_comp.ML
rename : src/HOL/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML
rename : src/HOL/BNF/Tools/bnf_decl.ML => src/HOL/Tools/BNF/Tools/bnf_decl.ML
rename : src/HOL/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/Tools/bnf_def.ML
rename : src/HOL/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML
rename : src/HOL/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML
rename : src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML
rename : src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML
rename : src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML
rename : src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML
rename : src/HOL/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/Tools/bnf_fp_util.ML
rename : src/HOL/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/Tools/bnf_gfp.ML
rename : src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML
rename : src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML
rename : src/HOL/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML
rename : src/HOL/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/Tools/bnf_lfp.ML
rename : src/HOL/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML
rename : src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML
rename : src/HOL/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML
rename : src/HOL/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML
rename : src/HOL/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/Tools/bnf_tactics.ML
rename : src/HOL/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/Tools/bnf_util.ML
|