src/HOL/Tools/inductive_codegen.ML
changeset 33726 0878aecbf119
parent 33522 737589bb9bb8
child 33771 17926df64f0f