src/HOL/add_ind_def.ML
changeset 1558 9c6ebfab4e05
parent 1465 5d7a7e439cec
child 2270 d7513875b2b8