1 use "../settings.ML";
2 no_document use_thy "While_Combinator";
3 use_thy "simp";
2 use_thy "simp";
4 use_thy "WFrec";
5 use_thy "Partial";