NEWS
changeset 50616 5b6cf0fbc329
parent 50592 a39250169636
child 50634 009a9fdabbad
     1.1 --- a/NEWS	Sat Dec 22 00:04:50 2012 +0100
     1.2 +++ b/NEWS	Sun Dec 23 19:54:15 2012 +0100
     1.3 @@ -217,6 +217,10 @@
     1.4    - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
     1.5      INCOMPATIBILITY
     1.6  
     1.7 +* HOL/Transitive_Closure: renamed lemmas
     1.8 +  reflcl_tranclp -> reflclp_tranclp
     1.9 +  rtranclp_reflcl -> rtranclp_reflclp
    1.10 +
    1.11  * HOL/Rings: renamed lemmas
    1.12  
    1.13  left_distrib ~> distrib_right