# HG changeset patch
# User chaieb
# Date 1204126896 -3600
# Node ID 3c0c69a65943bf0e9388642551e1bd1cb4c46fcc
# Parent  429c1917f07b12af669582900421a582f9d8d9fd
Fixed dependency on Dense_Linear_Order

diff -r 429c1917f07b -r 3c0c69a65943 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Wed Feb 27 16:07:55 2008 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Wed Feb 27 16:41:36 2008 +0100
@@ -8,7 +8,7 @@
 header {* Big O notation *}
 
 theory BigO
-imports Main SetsAndFunctions 
+imports Dense_Linear_Order Main SetsAndFunctions 
 begin
 
 subsection {* Definitions *}