equal
deleted
inserted
replaced
11 begin |
11 begin |
12 |
12 |
13 context includes no_Set_Product_syntax |
13 context includes no_Set_Product_syntax |
14 begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close> |
14 begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close> |
15 |
15 |
16 definition%important cross3 :: "[real^3, real^3] \<Rightarrow> real^3" (infixr "\<times>" 80) |
16 definition\<^marker>\<open>tag important\<close> cross3 :: "[real^3, real^3] \<Rightarrow> real^3" (infixr "\<times>" 80) |
17 where "a \<times> b \<equiv> |
17 where "a \<times> b \<equiv> |
18 vector [a$2 * b$3 - a$3 * b$2, |
18 vector [a$2 * b$3 - a$3 * b$2, |
19 a$3 * b$1 - a$1 * b$3, |
19 a$3 * b$1 - a$1 * b$3, |
20 a$1 * b$2 - a$2 * b$1]" |
20 a$1 * b$2 - a$2 * b$1]" |
21 |
21 |