src/HOL/Nominal/nominal_inductive2.ML
changeset 54783 25860d89a044
parent 51717 9e7d1c139569
child 54895 515630483010