src/HOL/Nominal/nominal_induct.ML
changeset 60299 5ae2a2e74c93
parent 59970 e9f73d87d904
child 60313 2a0b42cd58fb