--- 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*)
--- 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}%
%