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