src/HOL/Nominal/nominal_induct.ML
changeset 21379 a0561695167a
parent 20998 714a08286899
child 21879 a3efbae45735
equal deleted inserted replaced
21378:cedfce6fc725 21379:a0561695167a