use "../settings.ML"; use_thy "Typedef"; use_thy "Overloading0"; use_thy "Overloading2"; use_thy "Axioms";