src/HOL/Algebra/ROOT.ML
changeset 13870 cf947d1ec5ff
parent 9000 c20d58286a51
child 13936 d3671b878828
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Tue Mar 18 17:55:54 2003 +0100
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
     1.3 @@ -6,3 +6,4 @@
     1.4  
     1.5  with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
     1.6  with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
     1.7 +use_thy "Sylow";