src/HOL/Fun.thy
changeset 24471 d7cf53c1085f
parent 24286 7619080e49f0
child 25886 7753e0d81b7a