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