| changeset 69064 | 5840724b1d71 |
| parent 67399 | eab6ce8368fa |
| child 80914 | d97fdabd9e2b |
--- a/src/HOL/Library/ListVector.thy Sun Sep 23 21:49:31 2018 +0200 +++ b/src/HOL/Library/ListVector.thy Mon Sep 24 14:30:09 2018 +0200 @@ -13,7 +13,7 @@ text\<open>Multiplication with a scalar:\<close> abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70) -where "x *\<^sub>s xs \<equiv> map (( * ) x) xs" +where "x *\<^sub>s xs \<equiv> map ((*) x) xs" lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" by (induct xs) simp_all