src/HOL/Nominal/nominal_inductive2.ML
changeset 59487 adaa430fc0f7
parent 59058 a78612c67ec0
child 59498 50b60f501b05