src/HOL/Tools/Function/termination.ML
changeset 82086 e0edf30885ef
parent 81940 35d243b25ae2
equal deleted inserted replaced
82085:c0f4968fa96e 82086:e0edf30885ef