src/HOL/add_ind_def.ML
changeset 4176 84a0bfbd74e5
parent 4027 15768dba480e
child 4235 c4f1d3940d95
equal deleted inserted replaced
4175:06774cd43054 4176:84a0bfbd74e5