isabelle.in.tum.de;
authorwenzelm
Wed Jan 20 18:07:34 1999 +0100 (1999-01-20)
changeset 6148d97a944c6ea3
parent 6147 345c0fb3e628
child 6149 372919b37b5d
isabelle.in.tum.de;
Admin/page/index.html
doc-src/Logics/preface.tex
doc-src/System/present.tex
doc-src/Tutorial/basics.tex
doc-src/Tutorial/fp.tex
     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}