NEWS
changeset 62086 1c0246456ab9
parent 62084 969119292e25
child 62097 634838f919e4
equal deleted inserted replaced
62085:5b7758af429e 62086:1c0246456ab9
   643 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
   643 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
   644 Minor INCOMPATIBILITY, use 'function' instead.
   644 Minor INCOMPATIBILITY, use 'function' instead.
   645 
   645 
   646 * Library/Periodic_Fun: a locale that provides convenient lemmas for
   646 * Library/Periodic_Fun: a locale that provides convenient lemmas for
   647 periodic functions.
   647 periodic functions.
       
   648 
       
   649 * Library/Formal_Power_Series: proper definition of division (with remainder) 
       
   650 for formal power series; instances for Euclidean Ring and GCD.
   648 
   651 
   649 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
   652 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
   650 
   653 
   651 * HOL-Statespace: command 'statespace' uses mandatory qualifier for
   654 * HOL-Statespace: command 'statespace' uses mandatory qualifier for
   652 import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
   655 import of parent, as for general 'locale' expressions. INCOMPATIBILITY,