640 chain-complete partial orders. |
640 chain-complete partial orders. |
641 |
641 |
642 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. |
642 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. |
643 Minor INCOMPATIBILITY, use 'function' instead. |
643 Minor INCOMPATIBILITY, use 'function' instead. |
644 |
644 |
|
645 * Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions |
|
646 |
645 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= |
647 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= |
646 complex path integrals), Cauchy's integral theorem, winding numbers and |
648 complex path integrals), Cauchy's integral theorem, winding numbers and |
647 Cauchy's integral formula, Liouville theorem, Fundamental Theorem of |
649 Cauchy's integral formula, Liouville theorem, Fundamental Theorem of |
648 Algebra. Ported from HOL Light |
650 Algebra. Ported from HOL Light |
649 |
651 |
650 * Multivariate_Analysis: Added topological concepts such as connected |
652 * Multivariate_Analysis: Added topological concepts such as connected |
651 components, homotopic paths and the inside or outside of a set. |
653 components, homotopic paths and the inside or outside of a set. |
|
654 |
|
655 * Multivariate_Analysis: radius of convergence of power series and |
|
656 various summability tests; Harmonic numbers and the Euler–Mascheroni constant; |
|
657 the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/ |
|
658 Polygamma functions and their most important properties; |
652 |
659 |
653 * Data_Structures: new and growing session of standard data structures. |
660 * Data_Structures: new and growing session of standard data structures. |
654 |
661 |
655 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
662 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
656 |
663 |