src/HOL/Nominal/nominal_inductive.ML
changeset 55951 c07d184aebe9
parent 54991 1169c65e9698
child 56253 83b3c110f22d