# HG changeset patch
# User chaieb
# Date 1193829585 -3600
# Node ID 66ee31849d13ece950103337cb2fcfa1ef51bf8a
# Parent  0216ca99a599519089cffb49065c8bdacb01d3d9
Added example for the ideal membership problem solved by algebra

diff -r 0216ca99a599 -r 66ee31849d13 src/HOL/ex/Groebner_Examples.thy
--- 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