# 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 *}