src/HOL/Nominal/nominal_induct.ML
changeset 56153 2008f1cf3030
parent 55947 72db54a67152
child 58002 0ed1e999a0fb