src/HOL/Tools/Function/termination.ML
changeset 52727 ce51d6eb8f3d
parent 52723 2ebcc81f599c
child 52732 b4da1f2ec73f