src/HOL/Nominal/nominal_induct.ML
changeset 47534 06cc372a80ed
parent 45328 e5b33eecbf6e
child 51717 9e7d1c139569
equal deleted inserted replaced
47533:5afe54e05406 47534:06cc372a80ed