src/HOL/Nominal/nominal_inductive2.ML
changeset 44965 9e17d632a9ed
parent 44929 1886cddaf8a5
child 46218 ecf6375e2abb