src/HOL/Tools/function_package/termination.ML
changeset 20170 6ff853f82d73
parent 19806 f860b7a98445
child 20270 3abe7dae681e