src/HOL/Word/ROOT.ML
changeset 29628 d9294387ab0e
parent 28952 15a4b2cf8c34
child 33615 261abc2e3155
equal deleted inserted replaced
29627:152ace41f3fb 29628:d9294387ab0e
     1 no_document use_thys ["Infinite_Set"];
     1 use_thy "Word";
     2 use_thy "WordMain";