equal
deleted
inserted
replaced
1 (* ID: $Id$ |
1 (* Author: Tobias Nipkow, 2007 *) |
2 Author: Tobias Nipkow, 2007 |
|
3 *) |
|
4 |
2 |
5 header "Lists as vectors" |
3 header {* Lists as vectors *} |
6 |
4 |
7 theory ListVector |
5 theory ListVector |
8 imports Plain "~~/src/HOL/List" |
6 imports List Main |
9 begin |
7 begin |
10 |
8 |
11 text{* \noindent |
9 text{* \noindent |
12 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. |
13 Is only a vector space if restricted to lists of the same length. *} |
11 Is only a vector space if restricted to lists of the same length. *} |