src/HOL/add_ind_def.ML
changeset 2129 2ffe6e24f38d
parent 1465 5d7a7e439cec
child 2270 d7513875b2b8