src/HOL/Nominal/nominal_induct.ML
changeset 56916 b00a861d8f16
parent 55947 72db54a67152
child 58002 0ed1e999a0fb