src/HOL/Tools/Function/termination.ML
changeset 33448 7f716a975ada
parent 33099 b8cdd3d73022
child 33855 cd8acf137c9c