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 |
648 |
649 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= |
649 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
650 complex path integrals), Cauchy's integral theorem, winding numbers and |
650 |
651 Cauchy's integral formula, Liouville theorem, Fundamental Theorem of |
651 * HOL-Statespace: command 'statespace' uses mandatory qualifier for |
652 Algebra. Ported from HOL Light |
652 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
653 |
653 remove '!' and add '?' as required. |
654 * Multivariate_Analysis: Added topological concepts such as connected |
654 |
|
655 * HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour |
|
656 integrals (= complex path integrals), Cauchy's integral theorem, winding |
|
657 numbers and Cauchy's integral formula, Liouville theorem, Fundamental |
|
658 Theorem of Algebra. Ported from HOL Light. |
|
659 |
|
660 * HOL-Multivariate_Analysis: topological concepts such as connected |
655 components, homotopic paths and the inside or outside of a set. |
661 components, homotopic paths and the inside or outside of a set. |
656 |
662 |
657 * Multivariate_Analysis: radius of convergence of power series and |
663 * HOL-Multivariate_Analysis: radius of convergence of power series and |
658 various summability tests; Harmonic numbers and the Euler–Mascheroni |
664 various summability tests; Harmonic numbers and the Euler–Mascheroni |
659 constant; the Generalised Binomial Theorem; the complex and real |
665 constant; the Generalised Binomial Theorem; the complex and real |
660 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important |
666 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important |
661 properties. |
667 properties. |
662 |
668 |
663 * Probability: The central limit theorem based on Levy's uniqueness and |
669 * HOL-Probability: The central limit theorem based on Levy's uniqueness |
664 continuity theorems, weak convergence, and characterisitc functions. |
670 and continuity theorems, weak convergence, and characterisitc functions. |
665 |
671 |
666 * Data_Structures: new and growing session of standard data structures. |
672 * HOL-Data_Structures: new and growing session of standard data |
667 |
673 structures. |
668 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
|
669 |
|
670 * HOL-Statespace: command 'statespace' uses mandatory qualifier for |
|
671 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
|
672 remove '!' and add '?' as required. |
|
673 |
674 |
674 |
675 |
675 *** ML *** |
676 *** ML *** |
676 |
677 |
677 * The following combinators for low-level profiling of the ML runtime |
678 * The following combinators for low-level profiling of the ML runtime |