src/HOL/Tools/inductive_codegen.ML
changeset 41171 043f8dc3b51f
parent 40911 7febf76e0a69
child 41448 72ba43b47c7f