src/HOL/Nominal/nominal_inductive2.ML
changeset 54614 689398f0953f
parent 51717 9e7d1c139569
child 54895 515630483010