thys/NatBijection.thy
changeset 253 0846c45cedbb
parent 252 415e3082ccbc
child 254 0546ae452747