Admin/page/main-content/index.content
author wenzelm
Fri, 06 Oct 2000 16:11:53 +0200
changeset 10162 947b7b8b0a69
parent 10114 b07ed0c2f89f
child 11109 ce1cefc6c14c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     1
%title%
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     2
Isabelle
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     3
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     4
%body%
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     5
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     6
<p>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     7
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
     8
<h2>What is Isabelle?</h2>
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
     9
10019
wenzelm
parents: 10016
diff changeset
    10
Isabelle is a popular generic theorem proving environment developed at
wenzelm
parents: 10016
diff changeset
    11
Cambridge University (<a
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    12
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    13
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    14
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    15
<p>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    16
9285
21bfc8c14c3d about -> logics, better access to online libraries
kleing
parents: 8221
diff changeset
    17
These pages provide general information on Isabelle, more specific
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    18
information is available from the local pages
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    19
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    20
<ul>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    21
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    22
<li> <a
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    23
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    24
at Cambridge</strong></a> 
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    25
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    26
<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle at Munich</strong></a>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    27
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    28
</ul>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    29
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    30
See there for information on projects done with Isabelle, mailing list
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    31
archives, research papers, the Isabelle bibliography, and Isabelle
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    32
workshops and courses.
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    33
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    34
<p>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    36
<h2>Obtaining Isabelle</h2>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
10041
30693ebd16ae removed dead code;
wenzelm
parents: 10019
diff changeset
    38
The <strong><!-- _GP_ distname --></strong> distribution is available
30693ebd16ae removed dead code;
wenzelm
parents: 10019
diff changeset
    39
from several <a href="dist/index.html">mirror sites</a>.  It includes
30693ebd16ae removed dead code;
wenzelm
parents: 10019
diff changeset
    40
source and binary packages and browsable documentation.
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    41
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    42
<p>
9285
21bfc8c14c3d about -> logics, better access to online libraries
kleing
parents: 8221
diff changeset
    43
10019
wenzelm
parents: 10016
diff changeset
    44
You can also browse the <a href="library/index.html">Isabelle theory
wenzelm
parents: 10016
diff changeset
    45
library</a>; the main logics are <a
wenzelm
parents: 10016
diff changeset
    46
href="library/HOL/index.html">HOL</a>, <a
wenzelm
parents: 10016
diff changeset
    47
href="library/HOLCF/index.html">HOLCF</a>, <a
wenzelm
parents: 10016
diff changeset
    48
href="library/FOL/index.html">FOL</a> and <a
wenzelm
parents: 10016
diff changeset
    49
href="library/ZF/index.html">ZF</a>.
8070
dbbef2367723 some tuning (incorporated David's suggestions)
kleing
parents: 8060
diff changeset
    50
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    51
<p>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    52
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    53
<h2>Mailing list</h2>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    54
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    55
Use the mailing list <a href="mailto:
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    56
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> 
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    57
and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to
10162
wenzelm
parents: 10114
diff changeset
    58
discuss problems and results.  Why not <a
wenzelm
parents: 10114
diff changeset
    59
href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? 
10050
c8e0bd7a1e9c added headline, "quick download", and mailing list archive
kleing
parents: 10041
diff changeset
    60