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