| changeset 67968 | a5ad4c015d1c |
| parent 66884 | c2128ab11f61 |
| child 68651 | 16d98ef49a2c |
--- a/src/HOL/Analysis/Jordan_Curve.thy Sun Apr 08 12:31:08 2018 +0200 +++ b/src/HOL/Analysis/Jordan_Curve.thy Mon Apr 09 16:20:23 2018 +0200 @@ -9,7 +9,7 @@ begin -subsection\<open>Janiszewski's theorem.\<close> +subsection\<open>Janiszewski's theorem\<close> lemma Janiszewski_weak: fixes a b::complex