src/HOL/Library/ListVector.thy
 changeset 66453 cc19f7ca2ed6 parent 63882 018998c00003 child 67006 b1278ed3cd46
equal inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6
     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>