| changeset 42463 | f270e3e18be5 |
| parent 36753 | 5cf4e9128f22 |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/ex/Groebner_Examples.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/ex/Groebner_Examples.thy Sat Apr 23 13:00:19 2011 +0200 @@ -96,7 +96,7 @@ subsection {* Colinearity is invariant by rotation *} -types point = "int \<times> int" +type_synonym point = "int \<times> int" definition collinear ::"point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where "collinear \<equiv> \<lambda>(Ax,Ay) (Bx,By) (Cx,Cy).