src/HOL/add_ind_def.ML
changeset 3703 c5ae2d63dbaa
parent 2995 84df3b150b67
child 3768 67f4ac759100