doc-src/TutorialI/Types/Numbers.thy
changeset 27376 ffe9b958bada
parent 23504 2b2323124e8e
child 27658 674496eb5965
     1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Fri Jun 27 09:34:08 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Fri Jun 27 09:55:02 2008 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (* ID:         $Id$ *)
     1.5 -theory Numbers imports Real begin
     1.6 +theory Numbers
     1.7 +imports Complex_Main
     1.8 +begin
     1.9  
    1.10  ML "Pretty.setmargin 64"
    1.11  ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)