1.1 --- a/Admin/page/index.html Wed Jan 20 17:59:19 1999 +0100
1.2 +++ b/Admin/page/index.html Wed Jan 20 18:07:34 1999 +0100
1.3 @@ -7,7 +7,7 @@
1.4
1.5 <body>
1.6
1.7 -<h1>Isabelle </h1> <a href="http://www.in.tum.de/~isabelle/logo/"><img
1.8 +<h1>Isabelle </h1> <a href="http://isabelle.in.tum.de/logo/"><img
1.9 src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a>
1.10
1.11 <p>
1.12 @@ -23,13 +23,13 @@
1.13 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
1.14 src="cambridge.gif" width=145 border=0 align=right
1.15 alt="[Cambridge]"></a> <a
1.16 -href="http://www.in.tum.de/~isabelle/munich.html"><img
1.17 -src="munich.gif" width=48 border=0 align=right alt="[Munich]"></a>
1.18 -This page provides general information on Isabelle, more details are
1.19 -available on the local Isabelle pages at <a
1.20 +href="http://isabelle.in.tum.de/munich.html"><img src="munich.gif"
1.21 +width=48 border=0 align=right alt="[Munich]"></a> This page provides
1.22 +general information on Isabelle, more details are available on the
1.23 +local Isabelle pages at <a
1.24 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>
1.25 -and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>.
1.26 -See there for information on projects done with Isabelle, mailing list
1.27 +and <a href="http://isabelle.in.tum.de/munich.html">Munich</a>. See
1.28 +there for information on projects done with Isabelle, mailing list
1.29 archives, research papers, the Isabelle bibliography, and Isabelle
1.30 workshops and courses.
1.31
2.1 --- a/doc-src/Logics/preface.tex Wed Jan 20 17:59:19 1999 +0100
2.2 +++ b/doc-src/Logics/preface.tex Wed Jan 20 18:07:34 1999 +0100
2.3 @@ -49,7 +49,8 @@
2.4 distributed with Isabelle (see the directory \texttt{src}). They are
2.5 also available for browsing on the WWW at
2.6 \begin{ttbox}
2.7 -http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
2.8 +http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
2.9 +http://isabelle.in.tum.de/library/
2.10 \end{ttbox}
2.11 Note that this is not necessarily consistent with your local sources!
2.12
2.13 @@ -58,3 +59,7 @@
2.14 Manual} for more information on tactics, packages, etc.
2.15
2.16
2.17 +%%% Local Variables:
2.18 +%%% mode: latex
2.19 +%%% TeX-master: "logics"
2.20 +%%% End:
3.1 --- a/doc-src/System/present.tex Wed Jan 20 17:59:19 1999 +0100
3.2 +++ b/doc-src/System/present.tex Wed Jan 20 18:07:34 1999 +0100
3.3 @@ -56,7 +56,8 @@
3.4 A complete HTML version of all distributed Isabelle object-logics and
3.5 examples may be accessed on the WWW at:
3.6 \begin{ttbox}
3.7 -http://www4.informatik.tu-muenchen.de/~isabelle/library/
3.8 +http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
3.9 +http://isabelle.in.tum.de/library/
3.10 \end{ttbox}
3.11 Of course, this is not necessarily consistent with your local version!
3.12
4.1 --- a/doc-src/Tutorial/basics.tex Wed Jan 20 17:59:19 1999 +0100
4.2 +++ b/doc-src/Tutorial/basics.tex Wed Jan 20 18:07:34 1999 +0100
4.3 @@ -42,8 +42,12 @@
4.4 Everything defined in the parent theories (and their parents \dots) is
4.5 automatically visible. To avoid name clashes, identifiers can be qualified by
4.6 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
4.7 -available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is
4.8 -recommended browsing.
4.9 +available online at
4.10 +\begin{ttbox}
4.11 +http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/
4.12 +http://isabelle.in.tum.de/library/HOL/
4.13 +\end{ttbox}
4.14 +and is recommended browsing.
4.15 \begin{warn}
4.16 HOL contains a theory \ttindexbold{Main}, the union of all the basic
4.17 predefined theories like arithmetic, lists, sets, etc.\ (see the online
5.1 --- a/doc-src/Tutorial/fp.tex Wed Jan 20 17:59:19 1999 +0100
5.2 +++ b/doc-src/Tutorial/fp.tex Wed Jan 20 18:07:34 1999 +0100
5.3 @@ -355,19 +355,18 @@
5.4
5.5 \subsection{Lists}
5.6
5.7 -Lists are one of the essential datatypes in computing. Readers of this tutorial
5.8 -and users of HOL need to be familiar with their basic operations. Theory
5.9 -\texttt{ToyList} is only a small fragment of HOL's predefined theory
5.10 -\texttt{List}\footnote{\texttt{http://www.in.tum.de/\~\relax
5.11 - isabelle/library/HOL/List.html}}.
5.12 +Lists are one of the essential datatypes in computing. Readers of this
5.13 +tutorial and users of HOL need to be familiar with their basic operations.
5.14 +Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
5.15 +\texttt{List}\footnote{\texttt{http://isabelle.in.tum.de/library/HOL/List.html}}.
5.16 The latter contains many further operations. For example, the functions
5.17 \ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first
5.18 element and the remainder of a list. (However, pattern-matching is usually
5.19 -preferable to \texttt{hd} and \texttt{tl}.)
5.20 -Theory \texttt{List} also contains more syntactic sugar:
5.21 +preferable to \texttt{hd} and \texttt{tl}.) Theory \texttt{List} also
5.22 +contains more syntactic sugar:
5.23 \texttt{[}$x@1$\texttt{,}\dots\texttt{,}$x@n$\texttt{]} abbreviates
5.24 -$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}.
5.25 -In the rest of the tutorial we always use HOL's predefined lists.
5.26 +$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}. In the rest of the
5.27 +tutorial we always use HOL's predefined lists.
5.28
5.29
5.30 \subsection{The general format}