src/HOL/add_ind_def.ML
changeset 2351 873ffd6f70c3
parent 2270 d7513875b2b8
child 2859 7d640451ae7d