no_document use_thy "GCD"; use_thy "Examples1"; use_thy "Examples2"; setmp_noncritical quick_and_dirty true use_thy "Examples3";