src/HOL/Tools/Function/termination.ML
changeset 37035 4834c3112788
parent 35625 9c818cab0dd0
child 37387 3581483cca6c