equal
deleted
inserted
replaced
16 *} |
16 *} |
17 |
17 |
18 consts |
18 consts |
19 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) |
19 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) |
20 |
20 |
21 syntax (symbols) |
21 syntax (xsymbols) |
22 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) |
22 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) |
23 |
23 |
24 |
24 |
25 subsection {* Vector space laws *} |
25 subsection {* Vector space laws *} |
26 |
26 |