src/HOL/Algebra/ROOT.ML
changeset 13870 cf947d1ec5ff
parent 9000 c20d58286a51
child 13936 d3671b878828
equal deleted inserted replaced
13869:18112403c809 13870:cf947d1ec5ff
     4     Author: Clemens Ballarin, started 24 September 1999
     4     Author: Clemens Ballarin, started 24 September 1999
     5 *)
     5 *)
     6 
     6 
     7 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
     7 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
     8 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
     8 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
       
     9 use_thy "Sylow";