src/HOL/Library/ListVector.thy
changeset 61585 a9599d3d7610
parent 60500 903bb1495239
child 63882 018998c00003
     1.1 --- a/src/HOL/Library/ListVector.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/ListVector.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
     1.5  by (induct xs) simp_all
     1.6  
     1.7 -subsection \<open>@{text"+"} and @{text"-"}\<close>
     1.8 +subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
     1.9  
    1.10  fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.11  where