src/HOL/Tools/Function/termination.ML
changeset 54614 689398f0953f
parent 52732 b4da1f2ec73f
child 54742 7a86358a3c0b