# HG changeset patch
# User haftmann
# Date 1215759746 -7200
# Node ID f90a5775940d5061f9982fdc4048bb2bd0ad740e
# Parent  9bf0a22f8bcda3cda506a833dcca49186d10f346
explicit dependency

diff -r 9bf0a22f8bcd -r f90a5775940d src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Fri Jul 11 09:02:24 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Fri Jul 11 09:02:26 2008 +0200
@@ -9,7 +9,7 @@
 header {* Sequences and Convergence *}
 
 theory SEQ
-imports "../Real/Real"
+imports "../Real/Real" "../Real/ContNotDenum"
 begin
 
 definition