src/HOL/Fun.thy
changeset 75585 a789c5732f7a
parent 75583 451e17e0ba9d
child 75607 3c544d64c218