src/HOL/Library/Product_Lexorder.thy
2013-02-14 haftmann 2013-02-14 consolidation of library theories on product orders