use "../settings.ML"; use_thy "Tree"; use_thy "Tree2"; use_thy "Plus"; use_thy "case_exprs"; use_thy "fakenat"; use_thy "natsum"; use_thy "pairs"; use_thy "Option2"; use_thy "types"; use_thy "prime_def"; use_thy "simp"; use_thy "Itrev"; use_thy "AdvancedInd"; use_thy "appendix";