| changeset 70162 | 13b10ca71150 |
| parent 70160 | 8e9100dcde52 |
| child 80914 | d97fdabd9e2b |
--- a/src/HOL/Algebra/Indexed_Polynomials.thy Sat Apr 13 19:27:37 2019 +0100 +++ b/src/HOL/Algebra/Indexed_Polynomials.thy Sun Apr 14 11:59:54 2019 +0100 @@ -336,7 +336,7 @@ qed -subsection \<open>Link with Weak_Morphisms\<close> +subsection \<open>Link with Weak Morphisms\<close> text \<open>We study some elements of the contradiction needed in the algebraic closure existence proof. \<close>