src/HOL/Tools/Function/termination.ML
changeset 36603 d5d6111761a6
parent 35625 9c818cab0dd0
child 37387 3581483cca6c