src/HOL/Library/Product_ord.thy
changeset 30685 dd5fe091ff04
parent 28562 4e74209f113e
child 30738 0842e906300c