src/HOL/Nominal/nominal_inductive.ML
changeset 39970 9023b897e67a
parent 39557 fe5722fce758
child 41228 e1fce873b814