src/HOL/Nominal/nominal_inductive2.ML
changeset 75955 5305c65dcbb2
parent 74524 8ee3d5d3c1bf
child 78095 bc42c074e58f