src/HOL/Nominal/nominal_inductive2.ML
changeset 57987 ecb227b40907
parent 56253 83b3c110f22d
child 58112 8081087096ad