src/HOL/Nominal/nominal_inductive2.ML
changeset 77241 dd8f8445b8a4
parent 74524 8ee3d5d3c1bf
child 78095 bc42c074e58f