![[Isabelle logo]](isabelle.gif)
@@ -23,13 +23,13 @@
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">![[Cambridge]](cambridge.gif)
-This page provides general information on Isabelle, more details are
-available on the local Isabelle pages at
![[Munich]](munich.gif)
This page provides
+general information on Isabelle, more details are available on the
+local Isabelle pages at Cambridge
-and Munich.
-See there for information on projects done with Isabelle, mailing list
+and Munich. See
+there for information on projects done with Isabelle, mailing list
archives, research papers, the Isabelle bibliography, and Isabelle
workshops and courses.
diff -r 345c0fb3e628 -r d97a944c6ea3 doc-src/Logics/preface.tex
--- a/doc-src/Logics/preface.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Logics/preface.tex Wed Jan 20 18:07:34 1999 +0100
@@ -49,7 +49,8 @@
distributed with Isabelle (see the directory \texttt{src}). They are
also available for browsing on the WWW at
\begin{ttbox}
-http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
+http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
+http://isabelle.in.tum.de/library/
\end{ttbox}
Note that this is not necessarily consistent with your local sources!
@@ -58,3 +59,7 @@
Manual} for more information on tactics, packages, etc.
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "logics"
+%%% End:
diff -r 345c0fb3e628 -r d97a944c6ea3 doc-src/System/present.tex
--- a/doc-src/System/present.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/System/present.tex Wed Jan 20 18:07:34 1999 +0100
@@ -56,7 +56,8 @@
A complete HTML version of all distributed Isabelle object-logics and
examples may be accessed on the WWW at:
\begin{ttbox}
-http://www4.informatik.tu-muenchen.de/~isabelle/library/
+http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/
+http://isabelle.in.tum.de/library/
\end{ttbox}
Of course, this is not necessarily consistent with your local version!
diff -r 345c0fb3e628 -r d97a944c6ea3 doc-src/Tutorial/basics.tex
--- a/doc-src/Tutorial/basics.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Tutorial/basics.tex Wed Jan 20 18:07:34 1999 +0100
@@ -42,8 +42,12 @@
Everything defined in the parent theories (and their parents \dots) is
automatically visible. To avoid name clashes, identifiers can be qualified by
theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
-available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is
-recommended browsing.
+available online at
+\begin{ttbox}
+http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/
+http://isabelle.in.tum.de/library/HOL/
+\end{ttbox}
+and is recommended browsing.
\begin{warn}
HOL contains a theory \ttindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
diff -r 345c0fb3e628 -r d97a944c6ea3 doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Tutorial/fp.tex Wed Jan 20 18:07:34 1999 +0100
@@ -355,19 +355,18 @@
\subsection{Lists}
-Lists are one of the essential datatypes in computing. Readers of this tutorial
-and users of HOL need to be familiar with their basic operations. Theory
-\texttt{ToyList} is only a small fragment of HOL's predefined theory
-\texttt{List}\footnote{\texttt{http://www.in.tum.de/\~\relax
- isabelle/library/HOL/List.html}}.
+Lists are one of the essential datatypes in computing. Readers of this
+tutorial and users of HOL need to be familiar with their basic operations.
+Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
+\texttt{List}\footnote{\texttt{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
\ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first
element and the remainder of a list. (However, pattern-matching is usually
-preferable to \texttt{hd} and \texttt{tl}.)
-Theory \texttt{List} also contains more syntactic sugar:
+preferable to \texttt{hd} and \texttt{tl}.) Theory \texttt{List} also
+contains more syntactic sugar:
\texttt{[}$x@1$\texttt{,}\dots\texttt{,}$x@n$\texttt{]} abbreviates
-$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}.
-In the rest of the tutorial we always use HOL's predefined lists.
+$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}. In the rest of the
+tutorial we always use HOL's predefined lists.
\subsection{The general format}