src/HOL/Tools/Function/termination.ML
changeset 36516 8dac276ab10d
parent 35625 9c818cab0dd0
child 37387 3581483cca6c