src/HOL/Tools/function_package/termination.ML
changeset 21240 8e75fb38522c
parent 21237 b803f9870e97
child 21255 617fdb08abe9