# HG changeset patch
# User haftmann
# Date 1206738064 -3600
# Node ID 6deb216d726f8d84d20850c4e34c4c8d191082d3
# Parent  bb6a015219cf56fb8127b502725a86a605e8bd86
import Main explicitly

diff -r bb6a015219cf -r 6deb216d726f src/HOL/ex/Efficient_Nat_examples.thy
--- a/src/HOL/ex/Efficient_Nat_examples.thy	Fri Mar 28 22:01:03 2008 +0100
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Fri Mar 28 22:01:04 2008 +0100
@@ -6,7 +6,7 @@
 header {* Simple examples for Efficient\_Nat theory.  *}
 
 theory Efficient_Nat_examples
-imports "~~/src/HOL/Real/RealDef" Efficient_Nat
+imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
 begin
 
 fun