src/HOL/Fun.thy
changeset 59520 76d7c593c6e8
parent 59512 9bf568cc71a4
child 60303 00c06f1315d0