Loads Dense_Linear_Order (needed dlo_simps)
authorchaieb
Wed, 27 Feb 2008 15:35:43 +0100
changeset 26163 31e4ff2b9e5b
parent 26162 8dbf0e9d93d3
child 26164 429c1917f07b
Loads Dense_Linear_Order (needed dlo_simps)
src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Feb 27 15:35:42 2008 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Feb 27 15:35:43 2008 +0100
@@ -7,7 +7,7 @@
 header{*MacLaurin Series*}
 
 theory MacLaurin
-imports Transcendental
+imports Dense_Linear_Order Transcendental
 begin
 
 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}