NEWS
authorbulwahn
Fri Apr 13 09:17:01 2012 +0200 (2012-04-13)
changeset 47448cd3d987e8e79
parent 47447 22e64252eb35
child 47449 5e1482296b12
NEWS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu Apr 12 23:51:36 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Apr 13 09:17:01 2012 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* March 2012: Christian Sternagel, Japan Advanced Institute of Science and Technology
     1.8 +  Consolidated theory of relation composition.
     1.9 +
    1.10  * March 2012: Nik Sultana, University of Cambridge
    1.11    HOL/TPTP parser and import facilities.
    1.12  
     2.1 --- a/NEWS	Thu Apr 12 23:51:36 2012 +0200
     2.2 +++ b/NEWS	Fri Apr 13 09:17:01 2012 +0200
     2.3 @@ -294,6 +294,42 @@
     2.4   
     2.5  INCOMPATIBILITY.
     2.6  
     2.7 +* Theory Relation: Consolidated constant name for relation composition
     2.8 +  and corresponding theorem names:
     2.9 +  - Renamed constant rel_comp to relcomp
    2.10 +  - Dropped abbreviation pred_comp. Use relcompp instead.
    2.11 +  - Renamed theorems:
    2.12 +  Relation:
    2.13 +    rel_compI ~> relcompI
    2.14 +    rel_compEpair ~> relcompEpair
    2.15 +    rel_compE ~> relcompE
    2.16 +    pred_comp_rel_comp_eq ~> relcompp_relcomp_eq
    2.17 +    rel_comp_empty1 ~> relcomp_empty1
    2.18 +    rel_comp_mono ~> relcomp_mono
    2.19 +    rel_comp_subset_Sigma ~> relcomp_subset_Sigma
    2.20 +    rel_comp_distrib ~> relcomp_distrib
    2.21 +    rel_comp_distrib2 ~> relcomp_distrib2
    2.22 +    rel_comp_UNION_distrib ~> relcomp_UNION_distrib
    2.23 +    rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
    2.24 +    single_valued_rel_comp ~> single_valued_relcomp
    2.25 +    rel_comp_unfold ~> relcomp_unfold
    2.26 +    converse_rel_comp ~> converse_relcomp
    2.27 +    pred_compI ~> relcomppI
    2.28 +    pred_compE ~> relcomppE
    2.29 +    pred_comp_bot1 ~> relcompp_bot1
    2.30 +    pred_comp_bot2 ~> relcompp_bot2
    2.31 +    transp_pred_comp_less_eq ~> transp_relcompp_less_eq
    2.32 +    pred_comp_mono ~> relcompp_mono
    2.33 +    pred_comp_distrib ~> relcompp_distrib
    2.34 +    pred_comp_distrib2 ~> relcompp_distrib2
    2.35 +    converse_pred_comp ~> converse_relcompp
    2.36 +  Transitive_Closure:
    2.37 +    finite_rel_comp ~> finite_relcomp
    2.38 +  List:
    2.39 +    set_rel_comp ~> set_relcomp
    2.40 +
    2.41 +INCOMPATIBILITY.
    2.42 +
    2.43  * New theory HOL/Library/DAList provides an abstract type for association
    2.44    lists with distinct keys.
    2.45