src/HOL/Fun.thy
changeset 73888 9c2dd041477b
parent 73623 5020054b3a16
child 74101 d804e93ae9ff