src/HOL/add_ind_def.ML
changeset 1072 0140ff702b23
parent 923 ff1574a81019
child 1189 c17a8fd0c95d