src/HOL/Library/ListVector.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/ListVector.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/ListVector.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -1,16 +1,16 @@
     1.4  (*  Author: Tobias Nipkow, 2007 *)
     1.5  
     1.6 -section {* Lists as vectors *}
     1.7 +section \<open>Lists as vectors\<close>
     1.8  
     1.9  theory ListVector
    1.10  imports List Main
    1.11  begin
    1.12  
    1.13 -text{* \noindent
    1.14 +text\<open>\noindent
    1.15  A vector-space like structure of lists and arithmetic operations on them.
    1.16 -Is only a vector space if restricted to lists of the same length. *}
    1.17 +Is only a vector space if restricted to lists of the same length.\<close>
    1.18  
    1.19 -text{* Multiplication with a scalar: *}
    1.20 +text\<open>Multiplication with a scalar:\<close>
    1.21  
    1.22  abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
    1.23  where "x *\<^sub>s xs \<equiv> map (op * x) xs"
    1.24 @@ -18,7 +18,7 @@
    1.25  lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
    1.26  by (induct xs) simp_all
    1.27  
    1.28 -subsection {* @{text"+"} and @{text"-"} *}
    1.29 +subsection \<open>@{text"+"} and @{text"-"}\<close>
    1.30  
    1.31  fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.32  where