src/HOL/Nominal/nominal_inductive2.ML
changeset 62597 b3f2b8c906a6
parent 61144 5e94dfead1c2
child 62913 13252110a6fe