src/HOL/Nominal/nominal_inductive2.ML
changeset 39214 49fc6c842d6c
parent 39159 0dec18004e75
child 39557 fe5722fce758