NEWS
changeset 44015 a1507f567de6
parent 43970 3d204d261903
child 44018 d34f0cd62164
     1.1 --- a/NEWS	Tue Aug 02 11:52:57 2011 +0200
     1.2 +++ b/NEWS	Tue Aug 02 12:17:48 2011 +0200
     1.3 @@ -151,6 +151,12 @@
     1.4    - Use extended reals instead of positive extended reals.
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* Old recdef package has been moved to Library/Old_Recdef.thy, where it
     1.8 +must be loaded explicitly.  INCOMPATIBILITY.
     1.9 +
    1.10 +* Well-founded recursion combinator "wfrec" has been moved to
    1.11 +Library/Wfrec.thy. INCOMPATIBILY.
    1.12 +
    1.13  
    1.14  *** Document preparation ***
    1.15