src/HOL/Fun.thy
changeset 25345 dd5b851f8ef0
parent 24286 7619080e49f0
child 25886 7753e0d81b7a