equal
deleted
inserted
replaced
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, |