src/HOL/Tools/Function/termination.ML
changeset 46576 ae9286f64574
parent 46218 ecf6375e2abb
child 47433 07f4bf913230
equal deleted inserted replaced
46575:f1e387195a56 46576:ae9286f64574