src/HOL/Library/Product_ord.thy
changeset 44013 5cfc1c36ae97
parent 38857 97775f3e8722
child 44063 4588597ba37e
equal deleted inserted replaced
44012:8c1dfd6c2262 44013:5cfc1c36ae97