src/HOL/Algebra/Bij.thy
changeset 21505 13d4dba99337
parent 20318 0e0ea63fe768
child 27717 21bbd410ba04