| changeset 71201 | 6617fb368a06 |
| parent 71189 | 954ee5acaae0 |
| child 72560 | cd93b8c96710 |
| 71200:3548d54ce3ee | 71201:6617fb368a06 |
|---|---|
2 |
2 |
3 text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close> |
3 text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close> |
4 |
4 |
5 theory Great_Picard |
5 theory Great_Picard |
6 imports Conformal_Mappings |
6 imports Conformal_Mappings |
7 |
|
8 begin |
7 begin |
9 |
8 |
10 subsection\<open>Schottky's theorem\<close> |
9 subsection\<open>Schottky's theorem\<close> |
11 |
10 |
12 lemma Schottky_lemma0: |
11 lemma Schottky_lemma0: |