src/HOL/Tools/inductive_codegen.ML
changeset 27539 115d3a8bc6a6
parent 27398 768da1da59d6
child 27809 a1e409db516b