1 no_document use_thys ["Infinite_Set", "Parity"];
1 use_thy "WordExamples";
2 use_thy "WordExamples";
2