src/HOL/Tools/recfun_codegen.ML
changeset 42462 0fd80c27fdf5
parent 42411 ff997038e8eb
equal deleted inserted replaced
42461:56975de9e341 42462:0fd80c27fdf5