src/HOL/Nominal/nominal_induct.ML
changeset 45999 cce7e6197a46
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569
equal deleted inserted replaced
45998:d7cc533ae60d 45999:cce7e6197a46