diff -r 471b576aad25 -r 67268bb40b21 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 05 15:17:02 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 05 16:26:04 2007 +0200
@@ -85,23 +85,28 @@
   ATP_Linkup.thy Accessible_Part.thy Datatype.thy	\
   Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy		\
   FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy		\
-  Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
-  Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy\
-  OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy	\
-  Presburger.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy		\
-  Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy	\
-  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/reduce_axiomsN.ML	\
-  Tools/ATP/watcher.ML Tools/Presburger/cooper_dec.ML			\
-  Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML	\
-  Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML	\
+  Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy 	\
+  List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy 	\
+  Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy 	\
+  Predicate.thy Presburger.thy Product_Type.thy ROOT.ML Recdef.thy	\
+  Record.thy Refute.thy Relation.thy Relation_Power.thy			\
+  Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
+  Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML			\
+  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
+  Tools/Groebner_Basis/normalizer.ML					\
+  Tools/Groebner_Basis/normalizer_data.ML				\
+  Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML	\
+  Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML		\
+  Tools/Presburger/reflected_cooper.ML					\
   Tools/Presburger/reflected_presburger.ML Tools/TFL/dcterm.ML		\
   Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML			\
   Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML		\
   Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML	\
-  Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML\
-  Tools/datatype_hooks.ML Tools/datatype_package.ML			\
-  Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
-  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
+  Tools/datatype_aux.ML Tools/datatype_case.ML				\
+  Tools/datatype_codegen.ML Tools/datatype_hooks.ML			\
+  Tools/datatype_package.ML Tools/datatype_prop.ML			\
+  Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML		\
+  Tools/function_package/auto_term.ML					\
   Tools/function_package/context_tree.ML				\
   Tools/function_package/fundef_common.ML				\
   Tools/function_package/fundef_core.ML					\