src/HOL/Fun.thy
changeset 30505 110e59507eec
parent 30301 429612400fe9
child 31080 21ffc770ebc0