src/HOL/Nominal/nominal_inductive.ML
changeset 55400 1e8dd9cd320b
parent 54991 1169c65e9698
child 56253 83b3c110f22d