2016-02-17 blanchet [Wed, 17 Feb 2016 12:07:49 +0100] rev 62327
document new 'primrec' feature
NEWS src/Doc/Datatypes/Datatypes.thy

2016-02-17 blanchet [Wed, 17 Feb 2016 11:54:34 +0100] rev 62326
allow predicator instead of map function in 'primrec'
src/HOL/Nat.thy src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2016-02-16 traytel [Tue, 16 Feb 2016 22:28:19 +0100] rev 62325
simp rules for fsts, snds, setl, setr
src/HOL/BNF_Fixpoint_Base.thy

2016-02-16 traytel [Tue, 16 Feb 2016 22:28:19 +0100] rev 62324
make predicator a first-class bnf citizen
src/Doc/Datatypes/Datatypes.thy src/HOL/BNF_Composition.thy src/HOL/BNF_Def.thy src/HOL/Basic_BNFs.thy src/HOL/Cardinals/Bounded_Set.thy src/HOL/Library/Countable_Set_Type.thy src/HOL/Library/Dlist.thy src/HOL/Library/FSet.thy src/HOL/Library/Multiset.thy src/HOL/Library/bnf_axiomatization.ML src/HOL/Probability/Probability_Mass_Function.thy src/HOL/Tools/BNF/bnf_comp.ML src/HOL/Tools/BNF/bnf_comp_tactics.ML src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_def_tactics.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_gfp.ML src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/BNF/bnf_lfp_compat.ML src/HOL/Tools/BNF/bnf_lift.ML src/HOL/Tools/BNF/bnf_util.ML src/HOL/Tools/Lifting/lifting_bnf.ML src/HOL/Tools/Transfer/transfer_bnf.ML src/HOL/Transfer.thy

2016-02-16 blanchet [Tue, 16 Feb 2016 17:01:40 +0100] rev 62323
avoid duplicate theorems in 'primrec's result when invoked programmatically
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

2016-02-15 blanchet [Mon, 15 Feb 2016 18:27:17 +0100] rev 62322
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2016-02-15 blanchet [Mon, 15 Feb 2016 13:30:04 +0100] rev 62321
keep 'ctor_iff_dtor' theorem around in BNF FP database
src/HOL/Basic_BNF_LFPs.thy src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML

2016-02-15 blanchet [Mon, 15 Feb 2016 12:48:10 +0100] rev 62320
tuning
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2016-02-15 blanchet [Mon, 15 Feb 2016 12:47:52 +0100] rev 62319
rephrased message
src/HOL/Tools/Nitpick/nitpick.ML

2016-02-15 blanchet [Mon, 15 Feb 2016 12:47:35 +0100] rev 62318
clearer error message
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML