no_document use_thy "../Simple_Inductive_Package";+−