tuned proof;

--- a/src/HOL/ex/Groebner_Examples.thy	Tue Mar 18 20:33:31 2008 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy	Tue Mar 18 20:33:33 2008 +0100
@@ -99,7 +99,6 @@
   by (algebra add: collinear_def split_def fst_conv snd_conv)
 
 lemma "EX (d::int). a*y - a*x = n*d \<Longrightarrow> EX u v. a*u + n*v = 1 \<Longrightarrow> EX e. y - x = n*e"
-  apply algebra
-  done
+  by algebra
 
 end