src/HOL/Nominal/nominal_induct.ML
changeset 51085 d90218288d51
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569