src/HOL/Fun.thy
changeset 24710 141df8b68f63
parent 24286 7619080e49f0
child 25886 7753e0d81b7a