src/HOL/Fun.thy
changeset 69764 3ceff650adb9
parent 69735 8230dca028eb
child 69768 7e4966eaf781