src/HOL/Nominal/nominal_induct.ML
changeset 18396 b3e7da94b51f
parent 18311 b83b00cbaecf
child 18583 96e1ef2f806f