src/HOL/Nominal/nominal_inductive2.ML
changeset 75682 b6f3db86f9c7
parent 74524 8ee3d5d3c1bf
child 78095 bc42c074e58f