src/HOL/Tools/inductive_codegen.ML
changeset 22330 00ca68f5ce29
parent 22271 51a80e238b29
child 22360 26ead7ed4f4b