src/HOL/Nominal/nominal_inductive.ML
changeset 28500 4b79e5d3d0aa
parent 27847 0dffedf9aff5
child 29265 5b4247055bd7