src/HOL/Nominal/nominal_inductive.ML
changeset 43431 f3d5cecfecdc
parent 43326 47cf4bc789aa
child 44045 2814ff2a6e3e