src/HOL/Tools/Function/termination.ML
changeset 38797 abe92b33ac9f
parent 38795 848be46708dc
child 38864 4abe644fcea5