# HG changeset patch
# User chaieb
# Date 1204119596 -3600
# Node ID ff5bb2b532b3bfd3758ebdca28b5621af32e2c97
# Parent  ff372ff5cc34232e70fe9d0b0e7ed92a4e00926a
fixed dependencies

diff -r ff372ff5cc34 -r ff5bb2b532b3 src/HOL/ex/Dense_Linear_Order_Ex.thy
--- a/src/HOL/ex/Dense_Linear_Order_Ex.thy	Wed Feb 27 14:39:54 2008 +0100
+++ b/src/HOL/ex/Dense_Linear_Order_Ex.thy	Wed Feb 27 14:39:56 2008 +0100
@@ -6,7 +6,7 @@
 header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
 
 theory Dense_Linear_Order_Ex
-imports Main
+imports Dense_Linear_Order Main
 begin
 
 lemma