src/HOL/Fun.thy
changeset 53777 06a6216f733e
parent 52435 6646bb548c6b
child 53927 abe2b313f0e5