| changeset 27368 | 9f90ac19e32b | 
| parent 26806 | 40b411ec05aa | 
| child 27487 | c8a6ce181805 | 
--- a/src/HOL/Library/Order_Relation.thy Thu Jun 26 10:06:54 2008 +0200 +++ b/src/HOL/Library/Order_Relation.thy Thu Jun 26 10:07:01 2008 +0200 @@ -5,7 +5,7 @@ header {* Orders as Relations *} theory Order_Relation -imports ATP_Linkup Hilbert_Choice +imports Plain Hilbert_Choice ATP_Linkup begin text{* This prelude could be moved to theory Relation: *}