equal
deleted
inserted
replaced
592 |
592 |
593 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt |
593 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt |
594 fixpoint theorem for increasing functions in chain-complete partial |
594 fixpoint theorem for increasing functions in chain-complete partial |
595 orders. |
595 orders. |
596 |
596 |
597 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's |
597 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), |
598 integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light |
598 Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light |
599 |
599 |
600 * Multivariate_Analysis: Added topological concepts such as connected components, |
600 * Multivariate_Analysis: Added topological concepts such as connected components, |
601 homotopic paths and the inside or outside of a set. |
601 homotopic paths and the inside or outside of a set. |
602 |
602 |
603 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
603 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |