src/ZF/add_ind_def.ML
changeset 1868 836950047d85
parent 1735 96244c247b07
child 2033 639de962ded4