src/HOL/Nominal/nominal_inductive2.ML
changeset 51673 4dfa00e264d8
parent 50771 2852f997bfb5
child 51717 9e7d1c139569