equal
deleted
inserted
replaced
15 sort @{text "{plus, minus, zero}"} is considered, on which a real |
15 sort @{text "{plus, minus, zero}"} is considered, on which a real |
16 scalar multiplication @{text \<cdot>} is declared. |
16 scalar multiplication @{text \<cdot>} is declared. |
17 \<close> |
17 \<close> |
18 |
18 |
19 consts |
19 consts |
20 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) |
20 prod :: "real \<Rightarrow> 'a::{plus,minus,zero} \<Rightarrow> 'a" (infixr "\<cdot>" 70) |
21 |
|
22 notation (xsymbols) |
|
23 prod (infixr "\<cdot>" 70) |
|
24 notation (HTML output) |
|
25 prod (infixr "\<cdot>" 70) |
|
26 |
21 |
27 |
22 |
28 subsection \<open>Vector space laws\<close> |
23 subsection \<open>Vector space laws\<close> |
29 |
24 |
30 text \<open> |
25 text \<open> |