src/HOL/GroupTheory/ROOT.ML
changeset 13590 d8e98ef3ad13
parent 13583 5fcc8bf538ee
child 13745 a31e04831dd1
equal deleted inserted replaced
13589:b6d1a29dc978 13590:d8e98ef3ad13
     1 no_document use_thy "Primes";
     1 no_document use_thy "Primes";
     2 no_document use_thy "FuncSet";
     2 no_document use_thy "FuncSet";
     3 
     3 
     4 use_thy "Sylow";
     4 use_thy "Sylow";
     5 use_thy "Ring";
     5 use_thy "Module";