src/HOL/Nominal/nominal_inductive.ML
changeset 62836 98dbed6cfa44
parent 61144 5e94dfead1c2
child 62913 13252110a6fe