src/HOL/Nominal/nominal_inductive.ML
changeset 25318 c8352b38d47d
parent 24867 e5b55d7be9bb
child 25824 f56dd9745d1b