use "../settings.ML"; no_document use_thy "While_Combinator"; use_thy "simp"; use_thy "WFrec"; use_thy "Partial";