--- a/src/HOL/ex/Groebner_Examples.thy Wed Oct 31 12:19:44 2007 +0100
+++ b/src/HOL/ex/Groebner_Examples.thy Wed Oct 31 12:19:45 2007 +0100
@@ -6,7 +6,7 @@
header {* Groebner Basis Examples *}
theory Groebner_Examples
-imports Main
+imports Groebner_Basis
begin
subsection {* Basic examples *}
@@ -98,4 +98,8 @@
using assms
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
+
end