src/HOL/Nominal/nominal_induct.ML
changeset 28312 f0838044f034
parent 28083 103d9282a946
child 28965 1de908189869