src/ZF/add_ind_def.ML
changeset 5047 585fa380df1a
parent 4970 8b65444edbb0