src/HOL/Nominal/nominal_inductive2.ML
changeset 35669 a91c7ed801b8
parent 35232 f588e1169c8b
child 36323 655e2d74de3a