src/HOL/Nominal/nominal_inductive2.ML
changeset 29638 1f8f3d26a2cf
parent 29585 c23295521af5
child 30087 a780642a9c9c
child 30240 5b25fee0362c
equal deleted inserted replaced
29636:d01bada1df33 29638:1f8f3d26a2cf