src/HOL/Nominal/nominal_induct.ML
changeset 46312 518cc38a1a8c
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569