src/HOL/Fun.thy
changeset 30885 a3cfe0e27deb
parent 30301 429612400fe9
child 31080 21ffc770ebc0