src/HOL/add_ind_def.ML
changeset 3884 5423e06b9fe6
parent 3768 67f4ac759100
child 3945 ae9c61d69888
equal deleted inserted replaced
3883:acc1347cf2a0 3884:5423e06b9fe6