src/HOL/Nominal/nominal_inductive2.ML
changeset 44862 fe711df09fd9
parent 44689 f247fc952f31
child 44868 92be5b32ca71