# HG changeset patch
# User wenzelm
# Date 1205868813 -3600
# Node ID 01a98fd72eae5983fbf97e7e8992803d8ba54dcb
# Parent  9e9e67e33557251703df13f4f3aecdc460a0b188
tuned proof;

diff -r 9e9e67e33557 -r 01a98fd72eae src/HOL/ex/Groebner_Examples.thy
--- 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