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