src/HOL/Fun.thy
changeset 60149 9b0825a00b1a
parent 59512 9bf568cc71a4
child 60303 00c06f1315d0