src/HOL/Library/ListVector.thy
 changeset 67006 b1278ed3cd46 parent 66453 cc19f7ca2ed6 child 67399 eab6ce8368fa
equal 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>