NEWS
changeset 62098 b1b2834bb493
parent 62097 634838f919e4
child 62101 26c0a70f78a3
child 62107 f74a33b14200
     1.1 --- a/NEWS	Fri Jan 08 15:49:01 2016 +0100
     1.2 +++ b/NEWS	Fri Jan 08 15:54:43 2016 +0100
     1.3 @@ -568,10 +568,9 @@
     1.4      being defined.
     1.5    - Avoid various internal name clashes (e.g., 'datatype f = f').
     1.6  
     1.7 -* Transfer:
     1.8 -  - new methods for interactive debugging of 'transfer' and
     1.9 -    'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
    1.10 -    'transfer_prover_start' and 'transfer_prover_end'.
    1.11 +* Transfer: new methods for interactive debugging of 'transfer' and
    1.12 +'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
    1.13 +'transfer_prover_start' and 'transfer_prover_end'.
    1.14  
    1.15  * Division on integers is bootstrapped directly from division on
    1.16  naturals and uses generic numeral algorithm for computations. Slight
    1.17 @@ -651,8 +650,9 @@
    1.18  * Library/Periodic_Fun: a locale that provides convenient lemmas for
    1.19  periodic functions.
    1.20  
    1.21 -* Library/Formal_Power_Series: proper definition of division (with remainder) 
    1.22 -for formal power series; instances for Euclidean Ring and GCD.
    1.23 +* Library/Formal_Power_Series: proper definition of division (with
    1.24 +remainder) for formal power series; instances for Euclidean Ring and
    1.25 +GCD.
    1.26  
    1.27  * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.28