2016-02-15 wenzelm [Mon, 15 Feb 2016 14:55:44 +0100] rev 62337 Isabelle2016
proper syntax;
src/Doc/Isar_Ref/Quick_Reference.thy

2016-02-17 blanchet [Wed, 17 Feb 2016 17:21:43 +0100] rev 62336
tuning
src/Doc/Datatypes/Datatypes.thy

2016-02-17 blanchet [Wed, 17 Feb 2016 17:08:36 +0100] rev 62335
making 'pred_inject' a first-class BNF citizen
NEWS src/HOL/BNF_Fixpoint_Base.thy src/HOL/Basic_BNF_LFPs.thy src/HOL/Basic_BNFs.thy src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML src/HOL/Tools/BNF/bnf_fp_util.ML src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML src/HOL/Tools/Transfer/transfer_bnf.ML

2016-02-17 blanchet [Wed, 17 Feb 2016 17:08:03 +0100] rev 62334
refactoring
src/HOL/Tools/Transfer/transfer.ML src/HOL/Tools/Transfer/transfer_bnf.ML

2016-02-17 traytel [Wed, 17 Feb 2016 16:26:50 +0100] rev 62333
adjust 112eefe85ff0 to 532ad8de5d61
src/Doc/Datatypes/Datatypes.thy

2016-02-17 traytel [Wed, 17 Feb 2016 15:41:28 +0100] rev 62332
NEWS
NEWS

2016-02-17 traytel [Wed, 17 Feb 2016 15:18:06 +0100] rev 62331
correct (apparently untested) e1698a9578ea
src/Doc/Datatypes/Datatypes.thy

2016-02-17 traytel [Wed, 17 Feb 2016 15:18:06 +0100] rev 62330
document predicator in datatypes
src/Doc/Datatypes/Datatypes.thy

2016-02-17 traytel [Wed, 17 Feb 2016 15:18:06 +0100] rev 62329
derive transfer rule for predicator
src/HOL/BNF_Def.thy src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_def_tactics.ML src/HOL/Tools/Transfer/transfer_bnf.ML

2016-02-17 traytel [Wed, 17 Feb 2016 11:39:26 +0100] rev 62328
call the predicator of list list_all
src/Doc/Datatypes/Datatypes.thy src/HOL/List.thy