src/HOL/Library/ListVector.thy
changeset 67006 b1278ed3cd46
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
equal deleted inserted replaced
67005:11fca474d87a 67006:b1278ed3cd46
     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 HOL.List Main
     6 imports 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>