src/HOL/Fun.thy
changeset 69584 a91e32843310
parent 69502 0cf906072e20
child 69593 3dda49e08b9d