changeset 30663 | 0b6aff7451b2 |
parent 28562 | 4e74209f113e |
child 37765 | 26bdfb7b680b |
--- a/src/HOL/Library/Char_ord.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/Char_ord.thy Mon Mar 23 08:14:24 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/Char_ord.thy - ID: $Id$ Author: Norbert Voelker, Florian Haftmann *) header {* Order on characters *} theory Char_ord -imports Plain Product_ord Char_nat +imports Product_ord Char_nat Main begin instantiation nibble :: linorder