2013-04-24 blanchet [Wed, 24 Apr 2013 22:48:22 +0200] rev 51768
proper error generated for wrong mixfix
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 18:49:52 +0200] rev 51767
honor user-specified name for relator + generalize syntax
src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_fp.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_util.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 17:47:22 +0200] rev 51766
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
src/HOL/BNF/Examples/Stream.thy src/HOL/BNF/Examples/TreeFI.thy src/HOL/BNF/More_BNFs.thy src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_comp_tactics.ML src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_def_tactics.ML src/HOL/BNF/Tools/bnf_fp_def_sugar.ML src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_gfp_tactics.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_lfp_tactics.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 17:03:43 +0200] rev 51765
added "fundef_cong" attribute to "map_cong"
src/HOL/BNF/Tools/bnf_def.ML

2013-04-24 traytel [Wed, 24 Apr 2013 16:43:19 +0200] rev 51764
optimized proofs
src/HOL/Cardinals/Cardinal_Order_Relation.thy src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy src/HOL/Cardinals/Constructions_on_Wellorders.thy src/HOL/Cardinals/Constructions_on_Wellorders_Base.thy src/HOL/Cardinals/Fun_More.thy src/HOL/Cardinals/Fun_More_Base.thy src/HOL/Cardinals/Order_Relation_More.thy src/HOL/Cardinals/Order_Relation_More_Base.thy src/HOL/Cardinals/Wellorder_Embedding_Base.thy src/HOL/Cardinals/Wellorder_Relation.thy src/HOL/Cardinals/Wellorder_Relation_Base.thy

2013-04-24 blanchet [Wed, 24 Apr 2013 16:21:23 +0200] rev 51763
apply arguments to f and g in "case_cong"
src/HOL/BNF/Tools/bnf_wrap.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 15:42:00 +0200] rev 51762
derive "map_cong"
src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_def_tactics.ML src/HOL/BNF/Tools/bnf_fp.ML src/HOL/BNF/Tools/bnf_util.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 14:15:01 +0200] rev 51761
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"
src/HOL/BNF/Tools/bnf_comp.ML src/HOL/BNF/Tools/bnf_comp_tactics.ML src/HOL/BNF/Tools/bnf_def.ML src/HOL/BNF/Tools/bnf_def_tactics.ML src/HOL/BNF/Tools/bnf_gfp.ML src/HOL/BNF/Tools/bnf_gfp_tactics.ML src/HOL/BNF/Tools/bnf_lfp.ML src/HOL/BNF/Tools/bnf_lfp_tactics.ML src/HOL/BNF/Tools/bnf_tactics.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 14:14:36 +0200] rev 51760
killed dead code
src/HOL/BNF/Tools/bnf_util.ML

2013-04-24 blanchet [Wed, 24 Apr 2013 14:05:16 +0200] rev 51759
eta-contracted weak congruence rules (like in the old package)
src/HOL/BNF/Tools/bnf_wrap.ML