src/HOL/Nominal/nominal_inductive2.ML
changeset 57940 ca3be9612d85
parent 56253 83b3c110f22d
child 58112 8081087096ad