src/HOL/Tools/Function/termination.ML
changeset 35995 26e820d27e0a
parent 35625 9c818cab0dd0
child 37387 3581483cca6c