src/HOL/Fun.thy
changeset 24111 20e74aa5f56b
parent 24017 363287741ebe
child 24286 7619080e49f0