src/HOL/Nominal/nominal_induct.ML
changeset 35669 a91c7ed801b8
parent 34907 b0aaec87751c
child 36960 01594f816e3a