src/HOL/Nominal/nominal_inductive2.ML
changeset 66639 6a3cefd026fb
parent 65411 3c628937899d
child 67399 eab6ce8368fa