2014-03-06 blanchet [Thu, 06 Mar 2014 14:57:14 +0100] rev 55938
renamed 'set_rel' to 'rel_set'
NEWS src/HOL/BNF_Examples/Derivation_Trees/DTree.thy src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy src/HOL/Library/FSet.thy src/HOL/Library/Mapping.thy src/HOL/Lifting_Set.thy src/HOL/List.thy src/HOL/Topological_Spaces.thy src/HOL/ex/Transfer_Int_Nat.thy

2014-03-06 traytel [Thu, 06 Mar 2014 14:25:55 +0100] rev 55937
tuned
src/HOL/Tools/BNF/bnf_comp.ML

2014-03-06 traytel [Thu, 06 Mar 2014 14:15:09 +0100] rev 55936
rationalized imports
src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/BNF_Comp.thy src/HOL/BNF_FP_Base.thy src/HOL/BNF_Wellorder_Embedding.thy

2014-03-06 traytel [Thu, 06 Mar 2014 14:14:54 +0100] rev 55935
move special BNFs used for composition only to BNF_Comp;
use local copy of identity function that gets unfolded later for ID
src/HOL/BNF_Comp.thy src/HOL/Basic_BNFs.thy src/HOL/Tools/BNF/bnf_comp.ML

2014-03-06 blanchet [Thu, 06 Mar 2014 13:36:50 +0100] rev 55934
renamed 'cset_rel' to 'rel_cset'
NEWS src/HOL/Library/Countable_Set_Type.thy

2014-03-06 blanchet [Thu, 06 Mar 2014 13:36:49 +0100] rev 55933
renamed 'fset_rel' to 'rel_fset'
NEWS src/HOL/BNF_Examples/Derivation_Trees/DTree.thy src/HOL/BNF_Examples/TreeFsetI.thy src/HOL/Library/FSet.thy

2014-03-06 blanchet [Thu, 06 Mar 2014 13:36:48 +0100] rev 55932
renamed 'map_pair' to 'map_prod'
src/HOL/BNF_Examples/Lambda_Term.thy src/HOL/BNF_Examples/Misc_Primcorec.thy src/HOL/BNF_Examples/Misc_Primrec.thy src/HOL/BNF_Examples/Stream_Processor.thy src/HOL/BNF_FP_Base.thy src/HOL/Bali/State.thy src/HOL/Basic_BNFs.thy src/HOL/Cardinals/Ordinal_Arithmetic.thy src/HOL/Library/Code_Target_Int.thy src/HOL/Library/Quotient_Product.thy src/HOL/Lifting_Product.thy src/HOL/List.thy src/HOL/Matrix_LP/ComputeNumeral.thy src/HOL/Metis_Examples/Abstraction.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy src/HOL/Product_Type.thy src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_n2m.ML src/HOL/Tools/BNF/bnf_fp_util.ML src/HOL/Tools/Quickcheck/narrowing_generators.ML src/HOL/Wellfounded.thy src/HOL/ex/Coercion_Examples.thy

2014-03-06 blanchet [Thu, 06 Mar 2014 13:36:15 +0100] rev 55931
renamed 'map_sum' to 'sum_map'
NEWS src/HOL/BNF_Examples/Derivation_Trees/DTree.thy src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy src/HOL/BNF_FP_Base.thy src/HOL/Basic_BNFs.thy src/HOL/Cardinals/Ordinal_Arithmetic.thy src/HOL/HOLCF/Library/Option_Cpo.thy src/HOL/HOLCF/Library/Sum_Cpo.thy src/HOL/Library/Quotient_Sum.thy src/HOL/Lifting_Sum.thy src/HOL/Sum_Type.thy src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_n2m.ML src/HOL/Tools/BNF/bnf_fp_util.ML

2014-03-06 traytel [Thu, 06 Mar 2014 12:17:26 +0100] rev 55930
more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
src/HOL/BNF_Comp.thy src/HOL/BNF_FP_Base.thy src/HOL/Tools/BNF/bnf_comp.ML src/HOL/Tools/BNF/bnf_comp_tactics.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

2014-03-05 huffman [Wed, 05 Mar 2014 17:23:28 -0800] rev 55929
remove lemmas in favor of more general ones: convex(_hull)_set_{plus,setsum}
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy