src/HOL/Nominal/nominal_inductive.ML
changeset 25047 f8712e98756a
parent 24867 e5b55d7be9bb
child 25824 f56dd9745d1b