src/HOL/Nominal/nominal_induct.ML
changeset 71297 9f2085c499a2
parent 62178 c3c98ed94b0f
equal deleted inserted replaced
71296:71ea54e851ad 71297:9f2085c499a2