src/HOL/Nominal/nominal_inductive.ML
changeset 45999 cce7e6197a46
parent 44929 1886cddaf8a5
child 46218 ecf6375e2abb