src/HOL/Fun.thy
changeset 69419 8985ee17bfd2
parent 67399 eab6ce8368fa
child 69502 0cf906072e20