# HG changeset patch
# User chaieb
# Date 1181552757 -7200
# Node ID 6e32a5bfc30f4980f6eb3d544683211ba4db2672
# Parent  b1eb911bf22f96519080dc96cdfdfc780536b74b
explicitely depends on file groebner.ML

diff -r b1eb911bf22f -r 6e32a5bfc30f src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 11:05:56 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Mon Jun 11 11:05:57 2007 +0200
@@ -11,6 +11,7 @@
   "Tools/Groebner_Basis/misc.ML"
   "Tools/Groebner_Basis/normalizer_data.ML"
   ("Tools/Groebner_Basis/normalizer.ML")
+  ("Tools/Groebner_Basis/groebner.ML")
 begin
 
 subsection {* Semiring normalization *}