src/HOL/Fun.thy
changeset 33319 74f0dcc0b5fb
parent 33318 ddd97d9dfbfb
child 34101 d689f0b33047