src/HOL/Fun.thy
changeset 63412 def97df48390
parent 63400 249fa34faba2
child 63416 6af79184bef3