src/HOL/Nominal/nominal_inductive2.ML
changeset 76371 1ac2416e8432
parent 74524 8ee3d5d3c1bf
child 78095 bc42c074e58f