src/HOL/Nominal/nominal_induct.ML
changeset 64244 e7102c40783c
parent 62178 c3c98ed94b0f
equal deleted inserted replaced
64243:aee949f6642d 64244:e7102c40783c