src/HOL/Tools/function_package/termination.ML
changeset 21240 8e75fb38522c
parent 21237 b803f9870e97
child 21255 617fdb08abe9
equal deleted inserted replaced
21239:d4fbe2c87ef1 21240:8e75fb38522c