src/HOL/Fun.thy
changeset 73658 f6b453449cc6
parent 73623 5020054b3a16
child 74101 d804e93ae9ff