src/HOL/Tools/inductive_codegen.ML
changeset 43408 7e726f869de9
parent 43324 2b47822868e4
child 43619 3803869014aa