src/HOL/Tools/function_package/fundef_package.ML
changeset 23458 b2267a9e9e28
parent 23203 a5026e73cfcf
child 23473 997bca36d4fe
equal deleted inserted replaced
23457:53b788c014f8 23458:b2267a9e9e28