1.1 --- a/Admin/makebin	Mon May 12 19:54:43 2003 +0200
     1.2 +++ b/Admin/makebin	Tue May 13 08:59:21 2003 +0200
     1.3 @@ -112,15 +112,15 @@
     1.4    mkdir -p "heaps/$COMPILER/log"
     1.5    touch "heaps/$COMPILER/HOL"
     1.6    touch "heaps/$COMPILER/log/HOL.gz"
     1.7 -  touch "heaps/$COMPILER/HOL-Real"
     1.8 -  touch "heaps/$COMPILER/log/HOL-Real.gz"
     1.9 +  touch "heaps/$COMPILER/HOL-Complex"
    1.10 +  touch "heaps/$COMPILER/log/HOL-Complex.gz"
    1.11    touch "heaps/$COMPILER/ZF"
    1.12    touch "heaps/$COMPILER/log/ZF.gz"
    1.13    mkdir browser_info
    1.14  elif [ -n "$DO_LIBRARY" ]; then
    1.15    ./build -bait
    1.16  else
    1.17 -  ./build -b -m HOL-Real HOL
    1.18 +  ./build -b -m HOL-Complex HOL
    1.19    ./build -b ZF
    1.20    rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
    1.21  fi
    1.22 @@ -138,7 +138,7 @@
    1.23      gzip -f "${ISABELLE_NAME}_library.tar"
    1.24      cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
    1.25  else
    1.26 -  for IMG in HOL HOL-Real ZF
    1.27 +  for IMG in HOL HOL-Complex ZF
    1.28    do
    1.29      "$TAR" cf "${IMG}_$PLATFORM.tar" \
    1.30        "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \

     2.1 --- a/Admin/page/dist-content/packages.content	Mon May 12 19:54:43 2003 +0200
     2.2 +++ b/Admin/page/dist-content/packages.content	Tue May 13 08:59:21 2003 +0200
     2.3 @@ -65,9 +65,9 @@
     2.4  <!-- _GP_ download(3, "HOL", "HOL_x86-linux.tar.gz", "../..") -->
     2.5  <!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") -->
     2.6  <!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") -->
     2.7 -<!-- _GP_ download(3, "HOL-Real", "HOL-Real_x86-linux.tar.gz", "../..") -->
     2.8 -<!-- _GP_ download(0, "", "HOL-Real_sparc-solaris.tar.gz", "../..") -->
     2.9 -<!-- _GP_ download(0, "", "HOL-Real_ppc-darwin.tar.gz", "../..") -->
    2.10 +<!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") -->
    2.11 +<!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") -->
    2.12 +<!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") -->
    2.13  <!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
    2.14  <!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") -->
    2.15  <!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") -->

     3.1 --- a/INSTALL	Mon May 12 19:54:43 2003 +0200
     3.2 +++ b/INSTALL	Tue May 13 08:59:21 2003 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4  
     3.5  Special object-logic targets may be specified as follows:
     3.6  
     3.7 -  [ISABELLE_HOME]/build -m HOL-Real HOL
     3.8 +  [ISABELLE_HOME]/build -m HOL-Complex HOL
     3.9  
    3.10  
    3.11  2) User installation

     4.1 --- a/doc-src/HOL/HOL.tex	Mon May 12 19:54:43 2003 +0200
     4.2 +++ b/doc-src/HOL/HOL.tex	Tue May 13 08:59:21 2003 +0200
     4.3 @@ -1397,14 +1397,14 @@
     4.4  \subsection{Numerical types and numerical reasoning}
     4.5  
     4.6  The integers (type \tdx{int}) are also available in HOL, and the reals (type
     4.7 -\tdx{real}) are available in the logic image \texttt{HOL-Real}.  They support
     4.8 +\tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support
     4.9  the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
    4.10  multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the
    4.11  \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real
    4.12  division and other operations.  Both types belong to class \cldx{linorder}, so
    4.13  they inherit the relational operators and all the usual properties of linear
    4.14  orderings.  For full details, please survey the theories in subdirectories
    4.15 -\texttt{Integ} and \texttt{Real}.
    4.16 +\texttt{Integ}, \texttt{Real}, and \texttt{Complex}.
    4.17  
    4.18  All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
    4.19  where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.

     5.1 --- a/src/HOL/README.html	Mon May 12 19:54:43 2003 +0200
     5.2 +++ b/src/HOL/README.html	Tue May 13 08:59:21 2003 +0200
     5.3 @@ -28,15 +28,15 @@
     5.4  <dd>generic model of bytecode verification, i.e. data-flow analysis
     5.5  for assembly languages with subtypes
     5.6  
     5.7 -<dt>HOL-Real
     5.8 -<dd>a development of the reals and hyper-reals, which are used in
     5.9 -non-standard analysis (builds the image HOL-Real)
    5.10 +<dt>HOL-Complex
    5.11 +<dd>a development of the complex numbers, the reals, and the hyper-reals,
    5.12 +which are used in non-standard analysis (builds the image HOL-Complex)
    5.13  
    5.14 -<dt>HOL-Real-HahnBanach
    5.15 +<dt>HOL-Complex-HahnBanach
    5.16  <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    5.17  
    5.18 -<dt>HOL-Real-ex
    5.19 -<dd>miscellaneous real number examples
    5.20 +<dt>HOL-Complex-ex
    5.21 +<dd>miscellaneous real ans complex number examples
    5.22  
    5.23  <dt>Hoare
    5.24  <dd>verification of imperative programs (verification conditions are

     6.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon May 12 19:54:43 2003 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue May 13 08:59:21 2003 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4    shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
     6.5  proof (rule Zorn_Lemma2)
     6.6    txt_raw {* \footnote{See
     6.7 -  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}
     6.8 +  \url{http://isabelle.in.tum.de/library/HOL/HOL-Complex/Zorn.html}} \isanewline *}
     6.9    show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
    6.10    proof
    6.11      fix c assume "c \<in> chain S"