src/HOL/Fun.thy
changeset 68610 4fdc9f681479
parent 67399 eab6ce8368fa
child 69502 0cf906072e20