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