--- 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" \
--- 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", "../..") -->
--- 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
--- 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.
--- 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
--- 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"