# HG changeset patch
# User haftmann
# Date 1234807876 -3600
# Node ID a0e54cf21fd499ff9e65bdf7d99871dbee547522
# Parent  ffed4bd4bfad2c75f73e747e35a3753f6cd859d7
clarified import

diff -r ffed4bd4bfad -r a0e54cf21fd4 src/HOL/ex/Efficient_Nat_examples.thy
--- a/src/HOL/ex/Efficient_Nat_examples.thy	Mon Feb 16 19:11:16 2009 +0100
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Mon Feb 16 19:11:16 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/ex/Efficient_Nat_examples.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Simple examples for Efficient\_Nat theory. *}
 
 theory Efficient_Nat_examples
-imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
+imports Complex_Main Efficient_Nat
 begin
 
 fun to_n :: "nat \<Rightarrow> nat list" where