src/HOL/Nominal/nominal_inductive2.ML
changeset 32685 29e4e567b5f4
parent 32304 df010136264d
child 32952 aeb1e44fbc19