src/HOL/Library/Product_ord.thy
changeset 49695 8f61d1c7dded
parent 47961 e0a85be4fca0
equal deleted inserted replaced
49694:bdec6330acc4 49695:8f61d1c7dded