src/HOL/Fun.thy
changeset 55027 a74ea6d75571
parent 55019 0d5e831175de
child 55066 4e5ddf3162ac