src/HOL/Fun.thy
changeset 49890 89eff795f757
parent 49739 13aa6d8268ec
child 49905 a81f95693c68