src/HOL/Fun.thy
changeset 24261 dd31811bdf46
parent 24017 363287741ebe
child 24286 7619080e49f0