src/HOL/Fun.thy
changeset 25577 d739f48ef40c
parent 24286 7619080e49f0
child 25886 7753e0d81b7a