src/HOL/Nominal/nominal_inductive2.ML
changeset 29216 528e68bea04d
parent 28965 1de908189869
child 29265 5b4247055bd7