changeset 30738 | 0842e906300c |
parent 28562 | 4e74209f113e |
child 31040 | 996ae76c9eda |
--- a/src/HOL/Library/Product_ord.thy Fri Mar 27 10:05:08 2009 +0100 +++ b/src/HOL/Library/Product_ord.thy Fri Mar 27 10:05:11 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Product_ord.thy - ID: $Id$ Author: Norbert Voelker *) header {* Order on product types *} theory Product_ord -imports Plain +imports Main begin instantiation "*" :: (ord, ord) ord