src/HOL/Tools/function_package/fundef_common.ML
changeset 23424 d0580634f128
parent 23215 20b5558a5419
child 23766 77e796fe89eb
equal deleted inserted replaced
23423:b2d64f86d21b 23424:d0580634f128