src/HOL/Tools/recfun_codegen.ML
changeset 40973 890fefa597af
parent 40844 5895c525739d
child 41448 72ba43b47c7f
equal deleted inserted replaced
40972:ce78ef6a909b 40973:890fefa597af