src/HOL/Fun.thy
changeset 56547 e9bb73d7b6cf
parent 56154 f0a927235162
child 56608 8e3c848008fa