src/HOL/Nominal/nominal_inductive2.ML
changeset 36822 38a480e0346f
parent 36692 54b64d4ad524
child 36960 01594f816e3a