src/HOL/Tools/inductive_codegen.ML
changeset 19407 7c7a2e337504
parent 19046 bc5c6c9b114e
child 19861 620d90091788