src/HOL/Fun.thy
changeset 17421 0382f6877b98
parent 17084 fb0a80aef0be
child 17589 58eeffd73be1