# HG changeset patch
# User haftmann
# Date 1206738062 -3600
# Node ID fdd4d78e1e0566bee3be6fc1b13da050333e7474
# Parent  5d6b3a8081312658240985ab27a4ff012ac510bb
not depends on Main any longer

diff -r 5d6b3a808131 -r fdd4d78e1e05 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Mar 28 22:01:01 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Mar 28 22:01:02 2008 +0100
@@ -6,7 +6,7 @@
 header {* Implementation of natural numbers by target-language integers *}
 
 theory Efficient_Nat
-imports Main Code_Integer Code_Index
+imports Code_Integer Code_Index
 begin
 
 text {*