# HG changeset patch
# User haftmann
# Date 1214553302 -7200
# Node ID ffe9b958badaed3b9cdafe81025c54a310823f9a
# Parent  8d2c3d61c50260dd2cd9172ee7a03a7aa82c2b4f
adjusted import

diff -r 8d2c3d61c502 -r ffe9b958bada doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Fri Jun 27 09:34:08 2008 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Fri Jun 27 09:55:02 2008 +0200
@@ -1,5 +1,7 @@
 (* ID:         $Id$ *)
-theory Numbers imports Real begin
+theory Numbers
+imports Complex_Main
+begin
 
 ML "Pretty.setmargin 64"
 ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
diff -r 8d2c3d61c502 -r ffe9b958bada doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Fri Jun 27 09:34:08 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Fri Jun 27 09:55:02 2008 +0200
@@ -9,7 +9,9 @@
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ Numbers\ \isakeyword{imports}\ Real\ \isakeyword{begin}%
+\ Numbers\isanewline
+\isakeyword{imports}\ Complex{\isacharunderscore}Main\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %