src/HOL/Tools/recfun_codegen.ML
changeset 32815 1a5e364584ae
parent 32358 98c00ee9e786
child 32927 7a20fd22ba01
equal deleted inserted replaced
32814:81897d30b97f 32815:1a5e364584ae