src/HOL/Fun.thy
changeset 2647 83c9bdff7fdc
parent 1475 7f5a4cd08209
child 2912 3fac3e8d5d3e