| changeset 26165 | 3c0c69a65943 |
| parent 26041 | c2e15e65165f |
| child 26312 | e9a65675e5e8 |
--- 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 *}