clarified import
authorhaftmann
Mon, 16 Feb 2009 19:11:16 +0100
changeset 29938 a0e54cf21fd4
parent 29937 ffed4bd4bfad
child 29939 2138ff0ec94a
clarified import
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