src/HOL/Nominal/nominal_inductive2.ML
changeset 29981 7d0ed261b712
parent 29585 c23295521af5
child 30087 a780642a9c9c
child 30240 5b25fee0362c