src/HOL/Fun.thy
changeset 9369 139fde7af7bd
parent 9352 416b2ecd97a1
child 10212 33fe2d701ddd