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