src/HOL/Fun.thy
changeset 45982 989b1eede03c
parent 45603 d2d9ef16ccaf
child 46419 e139d0e29ca1