equal
deleted
inserted
replaced
1 (* Author: John Harrison |
1 (* Author: John Harrison |
2 Author: Robert Himmelmann, TU Muenchen (translation from HOL light) |
2 Author: Robert Himmelmann, TU Muenchen (translation from HOL light) |
3 *) |
3 *) |
4 |
4 |
5 section%important \<open>Fashoda Meet Theorem\<close> |
5 section \<open>Fashoda Meet Theorem\<close> |
6 |
6 |
7 theory Fashoda_Theorem |
7 theory Fashoda_Theorem |
8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space |
8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space |
9 begin |
9 begin |
10 |
10 |