src/HOL/add_ind_def.ML
changeset 2448 61337170db84
parent 2270 d7513875b2b8
child 2859 7d640451ae7d
equal deleted inserted replaced
2447:e86a6111cd8b 2448:61337170db84