src/HOL/Fun.thy
changeset 57124 e4c2c792226f
parent 56608 8e3c848008fa
child 57282 7da3e398804c