src/HOL/Nominal/nominal_induct.ML
changeset 26877 c3bb1f397811
parent 26712 e2dcda7b0401
child 26940 80df961f7900