# HG changeset patch
# User kleing
# Date 1052809161 -7200
# Node ID 213dcc39358faefae737f8e7d2eea67658e9eedf
# Parent  180f01d9df2c80d949f8a91c22ac3a8fe50c78fd
HOL-Real -> HOL-Complex

diff -r 180f01d9df2c -r 213dcc39358f Admin/makebin
--- a/Admin/makebin	Mon May 12 19:54:43 2003 +0200
+++ b/Admin/makebin	Tue May 13 08:59:21 2003 +0200
@@ -112,15 +112,15 @@
   mkdir -p "heaps/$COMPILER/log"
   touch "heaps/$COMPILER/HOL"
   touch "heaps/$COMPILER/log/HOL.gz"
-  touch "heaps/$COMPILER/HOL-Real"
-  touch "heaps/$COMPILER/log/HOL-Real.gz"
+  touch "heaps/$COMPILER/HOL-Complex"
+  touch "heaps/$COMPILER/log/HOL-Complex.gz"
   touch "heaps/$COMPILER/ZF"
   touch "heaps/$COMPILER/log/ZF.gz"
   mkdir browser_info
 elif [ -n "$DO_LIBRARY" ]; then
   ./build -bait
 else
-  ./build -b -m HOL-Real HOL
+  ./build -b -m HOL-Complex HOL
   ./build -b ZF
   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
 fi
@@ -138,7 +138,7 @@
     gzip -f "${ISABELLE_NAME}_library.tar"
     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
 else
-  for IMG in HOL HOL-Real ZF
+  for IMG in HOL HOL-Complex ZF
   do
     "$TAR" cf "${IMG}_$PLATFORM.tar" \
       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
diff -r 180f01d9df2c -r 213dcc39358f Admin/page/dist-content/packages.content
--- a/Admin/page/dist-content/packages.content	Mon May 12 19:54:43 2003 +0200
+++ b/Admin/page/dist-content/packages.content	Tue May 13 08:59:21 2003 +0200
@@ -65,9 +65,9 @@
 <!-- _GP_ download(3, "HOL", "HOL_x86-linux.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") -->
-<!-- _GP_ download(3, "HOL-Real", "HOL-Real_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL-Real_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL-Real_ppc-darwin.tar.gz", "../..") -->
+<!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") -->
 <!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") -->
diff -r 180f01d9df2c -r 213dcc39358f INSTALL
--- a/INSTALL	Mon May 12 19:54:43 2003 +0200
+++ b/INSTALL	Tue May 13 08:59:21 2003 +0200
@@ -65,7 +65,7 @@
 
 Special object-logic targets may be specified as follows:
 
-  [ISABELLE_HOME]/build -m HOL-Real HOL
+  [ISABELLE_HOME]/build -m HOL-Complex HOL
 
 
 2) User installation
diff -r 180f01d9df2c -r 213dcc39358f doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Mon May 12 19:54:43 2003 +0200
+++ b/doc-src/HOL/HOL.tex	Tue May 13 08:59:21 2003 +0200
@@ -1397,14 +1397,14 @@
 \subsection{Numerical types and numerical reasoning}
 
 The integers (type \tdx{int}) are also available in HOL, and the reals (type
-\tdx{real}) are available in the logic image \texttt{HOL-Real}.  They support
+\tdx{real}) are available in the logic image \texttt{HOL-Complex}.  They support
 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the
 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real
 division and other operations.  Both types belong to class \cldx{linorder}, so
 they inherit the relational operators and all the usual properties of linear
 orderings.  For full details, please survey the theories in subdirectories
-\texttt{Integ} and \texttt{Real}.
+\texttt{Integ}, \texttt{Real}, and \texttt{Complex}.
 
 All three numeric types admit numerals of the form \texttt{$sd\ldots d$},
 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.
diff -r 180f01d9df2c -r 213dcc39358f src/HOL/README.html
--- a/src/HOL/README.html	Mon May 12 19:54:43 2003 +0200
+++ b/src/HOL/README.html	Tue May 13 08:59:21 2003 +0200
@@ -28,15 +28,15 @@
 <dd>generic model of bytecode verification, i.e. data-flow analysis
 for assembly languages with subtypes
 
-<dt>HOL-Real
-<dd>a development of the reals and hyper-reals, which are used in
-non-standard analysis (builds the image HOL-Real)
+<dt>HOL-Complex
+<dd>a development of the complex numbers, the reals, and the hyper-reals,
+which are used in non-standard analysis (builds the image HOL-Complex)
 
-<dt>HOL-Real-HahnBanach
+<dt>HOL-Complex-HahnBanach
 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
 
-<dt>HOL-Real-ex
-<dd>miscellaneous real number examples
+<dt>HOL-Complex-ex
+<dd>miscellaneous real ans complex number examples
 
 <dt>Hoare
 <dd>verification of imperative programs (verification conditions are
diff -r 180f01d9df2c -r 213dcc39358f src/HOL/Real/HahnBanach/ZornLemma.thy
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon May 12 19:54:43 2003 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Tue May 13 08:59:21 2003 +0200
@@ -24,7 +24,7 @@
   shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z"
 proof (rule Zorn_Lemma2)
   txt_raw {* \footnote{See
-  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}
+  \url{http://isabelle.in.tum.de/library/HOL/HOL-Complex/Zorn.html}} \isanewline *}
   show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
   proof
     fix c assume "c \<in> chain S"