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 (xsymbols) |
21 const_syntax (xsymbols) |
22 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) |
22 prod (infixr "\<cdot>" 70) |
23 syntax (HTML output) |
23 const_syntax (HTML output) |
24 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70) |
24 prod (infixr "\<cdot>" 70) |
25 |
25 |
26 |
26 |
27 subsection {* Vector space laws *} |
27 subsection {* Vector space laws *} |
28 |
28 |
29 text {* |
29 text {* |