--- a/src/HOL/Algebra/ROOT.ML Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/Algebra/ROOT.ML Tue Mar 18 18:07:06 2003 +0100
@@ -6,3 +6,4 @@
with_path "abstract" time_use_thy "Abstract"; (*The ring theory*)
with_path "poly" time_use_thy "Polynomial"; (*The full theory*)
+use_thy "Sylow";