src/HOL/Tools/Function/termination.ML
changeset 47486 4d49f3ffe97e
parent 47433 07f4bf913230
child 47835 2d48bf79b725