src/HOL/Fun.thy
changeset 17970 a84ac7c201ea
parent 17956 369e2af8ee45
child 18154 0c05abaf6244