equal
deleted
inserted
replaced
94 by (algebra add: sq_def) |
94 by (algebra add: sq_def) |
95 |
95 |
96 |
96 |
97 subsection {* Colinearity is invariant by rotation *} |
97 subsection {* Colinearity is invariant by rotation *} |
98 |
98 |
99 types point = "int \<times> int" |
99 type_synonym point = "int \<times> int" |
100 |
100 |
101 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where |
101 definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where |
102 "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy). |
102 "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy). |
103 ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" |
103 ((Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx))" |
104 |
104 |