src/HOL/Nominal/nominal_inductive.ML
changeset 78130 8234c42d20e6
parent 78097 2ea20bb1493c
child 78806 aca84704d46f