src/HOL/Tools/Function/termination.ML
changeset 46623 bce24d3f29e7
parent 46218 ecf6375e2abb
child 47433 07f4bf913230