equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow, 2007 *) |
1 (* Author: Tobias Nipkow, 2007 *) |
2 |
2 |
3 section \<open>Lists as vectors\<close> |
3 section \<open>Lists as vectors\<close> |
4 |
4 |
5 theory ListVector |
5 theory ListVector |
6 imports List Main |
6 imports HOL.List Main |
7 begin |
7 begin |
8 |
8 |
9 text\<open>\noindent |
9 text\<open>\noindent |
10 A vector-space like structure of lists and arithmetic operations on them. |
10 A vector-space like structure of lists and arithmetic operations on them. |
11 Is only a vector space if restricted to lists of the same length.\<close> |
11 Is only a vector space if restricted to lists of the same length.\<close> |