src/HOL/Fun.thy
changeset 24729 f5015dd2431b
parent 24286 7619080e49f0
child 25886 7753e0d81b7a