src/HOL/Nominal/nominal_inductive2.ML
changeset 40858 69ab03d29c92
parent 39557 fe5722fce758
child 41228 e1fce873b814