src/HOL/Nominal/nominal_inductive2.ML
changeset 33960 53993394ac19
parent 33772 b6a1feca2ac2
child 33968 f94fb13ecbb3