src/ZF/add_ind_def.ML
changeset 1933 8b24773de6db
parent 1735 96244c247b07
child 2033 639de962ded4
equal deleted inserted replaced
1932:cc9f1ba8f29a 1933:8b24773de6db