src/HOL/Tools/recfun_codegen.ML
changeset 24930 cc2e0e8c81af
parent 24907 bfb2e82b61fe
child 25389 3e58c7cb5a73
equal deleted inserted replaced
24929:408becab067e 24930:cc2e0e8c81af