# HG changeset patch
# User chaieb
# Date 1204122943 -3600
# Node ID 31e4ff2b9e5bb38712a8e67b017f25cdbc122d11
# Parent  8dbf0e9d93d3a5ac6bd252582274d9cdef7df3fa
Loads Dense_Linear_Order (needed dlo_simps)

diff -r 8dbf0e9d93d3 -r 31e4ff2b9e5b 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*}