src/HOL/Fun.thy
changeset 59527 edaabc1ab1ed
parent 59512 9bf568cc71a4
child 60303 00c06f1315d0