src/HOL/Nominal/nominal_inductive2.ML
changeset 29833 409138c4de12
parent 29585 c23295521af5
child 30087 a780642a9c9c
child 30240 5b25fee0362c