src/HOL/Tools/Function/termination.ML
changeset 37313 715d25555ca6
parent 35625 9c818cab0dd0
child 37387 3581483cca6c