src/HOL/Library/Product_Lexorder.thy
changeset 58798 49ed5eea15d4
parent 54863 82acc20ded73
child 58881 b9556a055632