src/HOL/Nominal/nominal_inductive.ML
changeset 32527 569e8d6729a1
parent 32202 443d5cfaba1b
child 32952 aeb1e44fbc19