src/HOL/Nominal/nominal_induct.ML
changeset 58149 72fc2bf52986
parent 58002 0ed1e999a0fb
child 58957 c9e744ea8a38