src/HOL/Nominal/nominal_induct.ML
changeset 49489 f59475e6589f
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569