src/HOL/Nominal/nominal_induct.ML
changeset 41648 6d736d983d5c
parent 37137 bac3d00a910a
child 42361 23f352990944