consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
authorhaftmann
Fri, 06 Jan 2012 21:48:45 +0100
changeset 470160ec0af1c651d
parent 47015 cc374091999b
child 47017 6baea4fca6bd
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
NEWS
     1.1 --- a/NEWS	Fri Jan 06 20:48:52 2012 +0100
     1.2 +++ b/NEWS	Fri Jan 06 21:48:45 2012 +0100
     1.3 @@ -60,6 +60,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Consolidated various theorem names relating to Finite_Set.fold combinator:
     1.8 +  inf_INFI_fold_inf ~> inf_INF_fold_inf
     1.9 +  sup_SUPR_fold_sup ~> sup_SUP_fold_sup
    1.10 +  INFI_fold_inf ~> INF_fold_inf
    1.11 +  SUPR_fold_sup ~> SUP_fold_sup
    1.12 +  union_set ~> union_set_fold
    1.13 +  minus_set ~> minus_set_fold
    1.14 +  
    1.15 +INCOMPATIBILITY.
    1.16 +
    1.17  * Consolidated theorem names concerning fold combinators:
    1.18    INFI_set_fold ~> INF_set_fold
    1.19    SUPR_set_fold ~> SUP_set_fold