changeset 71031 | 66c025383422 |
parent 70817 | dd675800469d |
child 71032 | acedd04c1a42 |
--- a/src/HOL/Analysis/Winding_Numbers.thy Mon Nov 04 19:53:43 2019 -0500 +++ b/src/HOL/Analysis/Winding_Numbers.thy Tue Nov 05 13:56:22 2019 +0100 @@ -3,7 +3,10 @@ text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2017)\<close> theory Winding_Numbers -imports Polytope Jordan_Curve Riemann_Mapping +imports + Polytope + Jordan_Curve + Riemann_Mapping begin lemma simply_connected_inside_simple_path: