# HG changeset patch
# User haftmann
# Date 1214552048 -7200
# Node ID 8d2c3d61c50260dd2cd9172ee7a03a7aa82c2b4f
# Parent  2a3c22fd95ab72544fca7adaed66961c3753b59a
adjusted import

diff -r 2a3c22fd95ab -r 8d2c3d61c502 doc-src/Locales/Locales/Examples.thy
--- a/doc-src/Locales/Locales/Examples.thy	Fri Jun 27 00:37:30 2008 +0200
+++ b/doc-src/Locales/Locales/Examples.thy	Fri Jun 27 09:34:08 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory Examples
-imports GCD
+imports Main GCD
 begin
 
 hide %invisible const Lattices.lattice
diff -r 2a3c22fd95ab -r 8d2c3d61c502 doc-src/Locales/Locales/document/Examples.tex
--- a/doc-src/Locales/Locales/document/Examples.tex	Fri Jun 27 00:37:30 2008 +0200
+++ b/doc-src/Locales/Locales/document/Examples.tex	Fri Jun 27 09:34:08 2008 +0200
@@ -11,7 +11,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ Examples\isanewline
-\isakeyword{imports}\ GCD\isanewline
+\isakeyword{imports}\ Main\ GCD\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%