src/HOL/Tools/inductive_codegen.ML
changeset 19599 a5c7eb37d14f
parent 19046 bc5c6c9b114e
child 19861 620d90091788