src/ZF/add_ind_def.ML
changeset 2334 00db792beb4e
parent 2266 82aef6857c5b
child 2871 ba585d52ea4e