changeset 69683 | 8b3458ca0762 |
parent 69632 | 7d02b7bee660 |
child 69730 | 0c3dcb3a17f6 |
69682:500a7acdccd4 | 69683:8b3458ca0762 |
---|---|
1 subsection%important \<open>Ordered Euclidean Space\<close> |
1 subsection \<open>Ordered Euclidean Space\<close> |
2 |
2 |
3 theory Ordered_Euclidean_Space |
3 theory Ordered_Euclidean_Space |
4 imports |
4 imports |
5 Cartesian_Euclidean_Space |
5 Cartesian_Euclidean_Space |
6 "HOL-Library.Product_Order" |
6 "HOL-Library.Product_Order" |