equal
deleted
inserted
replaced
1 (* Title: Vector_Spaces.thy |
1 (* Title: HOL/Vector_Spaces.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 |
9 section \<open>Vector Spaces\<close> |
9 section \<open>Vector Spaces\<close> |
10 |
10 |
11 theory Vector_Spaces |
11 theory Vector_Spaces |