src/HOL/add_ind_def.ML
changeset 3718 d78cf498a88c
parent 2995 84df3b150b67
child 3768 67f4ac759100