equal
deleted
inserted
replaced
1 (* Title: Cartesian_Space.thy |
1 (* Title: HOL/Analysis/Cartesian_Space.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 Author: Jose Divasón <jose.divasonm at unirioja.es> |
3 Author: Jose Divasón <jose.divasonm at unirioja.es> |
4 Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> |
4 Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> |
5 Author: Johannes Hölzl, VU Amsterdam |
5 Author: Johannes Hölzl, VU Amsterdam |
6 Author: Fabian Immler, TUM |
6 Author: Fabian Immler, TUM |
7 *) |
7 *) |
|
8 |
8 theory Cartesian_Space |
9 theory Cartesian_Space |
9 imports |
10 imports |
10 Finite_Cartesian_Product Linear_Algebra |
11 Finite_Cartesian_Product Linear_Algebra |
11 begin |
12 begin |
12 |
13 |