src/HOL/Nominal/nominal_inductive.ML
changeset 33967 e191b400a8e0
parent 33772 b6a1feca2ac2
child 33968 f94fb13ecbb3