src/HOL/Fun.thy
changeset 67697 58f951ce71c8
parent 67399 eab6ce8368fa
child 69502 0cf906072e20