src/ZF/add_ind_def.ML
changeset 3778 b70c41bc7491
parent 3768 67f4ac759100
child 3925 90f499226ab9