src/HOL/Nominal/nominal_inductive.ML
changeset 57987 ecb227b40907
parent 57884 36b5691b81a5
child 58112 8081087096ad