src/HOL/Nominal/nominal_inductive.ML
changeset 59912 c7ba9b133bd4
parent 59621 291934bac95e
child 59936 b8ffc3dc9e24