src/HOL/Nominal/nominal_induct.ML
changeset 36632 f96aa31b739d
parent 34907 b0aaec87751c
child 36960 01594f816e3a