src/HOL/Fun.thy
changeset 81545 6f8a56a6b391
parent 81182 fc5066122e68
child 81563 c4c983c5c7f2