src/HOL/Library/ListVector.thy
changeset 66453 cc19f7ca2ed6
parent 63882 018998c00003
child 67006 b1278ed3cd46
equal deleted 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>