src/HOL/Library/Product_Lexorder.thy
changeset 58187 d2ddd401d74d
parent 54863 82acc20ded73
child 58881 b9556a055632