src/HOL/Tools/inductive_codegen.ML
changeset 40913 99a4ef20704d
parent 40911 7febf76e0a69
child 41448 72ba43b47c7f
equal deleted inserted replaced
40912:1108529100ce 40913:99a4ef20704d