src/HOL/Nominal/nominal_induct.ML
changeset 35180 c57dba973391
parent 34907 b0aaec87751c
child 36960 01594f816e3a