| changeset 55018 | 2a526bd279ed |
| parent 54230 | b1d955791529 |
| child 57512 | cc97b347b301 |
| 55017:2df6ad1dbd66 | 55018:2a526bd279ed |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Vector spaces *} |
5 header {* Vector spaces *} |
6 |
6 |
7 theory Vector_Space |
7 theory Vector_Space |
8 imports Complex_Main Bounds "~~/src/HOL/Library/Zorn" |
8 imports Complex_Main Bounds |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Signature *} |
11 subsection {* Signature *} |
12 |
12 |
13 text {* |
13 text {* |