src/HOL/Library/Product_ord.thy
changeset 29216 528e68bea04d
parent 28562 4e74209f113e
child 30738 0842e906300c
equal deleted inserted replaced
29215:f98862eb0591 29216:528e68bea04d