src/HOL/Tools/inductive.ML
changeset 44928 7ef6505bde7f
parent 44868 92be5b32ca71
child 45290 f599ac41e7f5