src/HOL/Fun.thy
changeset 26100 fbc60cd02ae2
parent 25886 7753e0d81b7a
child 26105 ae06618225ec