| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
97b25dd9 |
|
17-Feb-2016 |
blanchet <none@none> |
making 'pred_inject' a first-class BNF citizen
|
| #
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;
|
| #
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;
|
| #
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
|
| #
462f1580 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned proofs
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
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'
|
| #
c7dca0cc |
|
06-Mar-2014 |
traytel <none@none> |
move special BNFs used for composition only to BNF_Comp;
use local copy of identity function that gets unfolded later for ID
|
| #
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'
|
| #
bbeeaf3d |
|
28-Feb-2014 |
traytel <none@none> |
load Metis a little later
|
| #
8585a8d9 |
|
24-Feb-2014 |
traytel <none@none> |
clarified interaction with dead variables in the composition of BNFs
|
| #
2312c694 |
|
20-Jan-2014 |
blanchet <none@none> |
rationalized lemmas
|
| #
e3355c3e |
|
20-Jan-2014 |
blanchet <none@none> |
move BNF_LFP up the dependency chain
|
| #
41c735bc |
|
20-Jan-2014 |
blanchet <none@none> |
dissolved BNF session
--HG--
rename : src/HOL/BNF/BNF_Decl.thy => src/HOL/Library/BNF_Decl.thy
rename : src/HOL/Cardinals/Cardinal_Notations.thy => src/HOL/Library/Cardinal_Notations.thy
rename : src/HOL/BNF/Countable_Set_Type.thy => src/HOL/Library/Countable_Set_Type.thy
rename : src/HOL/BNF/More_BNFs.thy => src/HOL/Library/More_BNFs.thy
rename : src/HOL/BNF/Tools/bnf_decl.ML => src/HOL/Library/bnf_decl.ML
|
| #
b575b3f0 |
|
20-Jan-2014 |
blanchet <none@none> |
made BNF compile after move to HOL
|
| #
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
|