src/HOL/Tools/inductive_codegen.ML
changeset 27793 29ad1d91a5a3
parent 27398 768da1da59d6
child 27809 a1e409db516b