src/HOL/Nominal/nominal_induct.ML
changeset 57987 ecb227b40907
parent 55947 72db54a67152
child 58002 0ed1e999a0fb
equal deleted inserted replaced
57986:0d60b9e58487 57987:ecb227b40907