src/HOL/Library/Product_ord.thy
changeset 25559 f14305fb698c
parent 25502 9200b36280c0
child 25571 c9e39eafc7a0