src/HOL/Nominal/nominal_inductive2.ML
changeset 32936 9491bec20595
parent 32304 df010136264d
child 32952 aeb1e44fbc19