src/HOL/Nominal/nominal_inductive2.ML
changeset 66308 b6a0d95b94be
parent 65411 3c628937899d
child 67399 eab6ce8368fa