src/HOL/Nominal/nominal_induct.ML
changeset 25381 c100bf5bd6b8
parent 24920 2a45e400fdad
child 25985 8d69087f6a4b