src/HOL/Nominal/nominal_inductive.ML
changeset 58650 1ddba8bcbb58
parent 58112 8081087096ad
child 59058 a78612c67ec0