lib/logo/index.html
author webertj
Mon, 07 Mar 2005 19:41:04 +0100
changeset 15585 513aa9a3a26d
parent 7807 6a102f74ad0a
child 28504 7ad7d7d6df47
permissions -rw-r--r--
HTML 4.01 Transitional conformity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
     2
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
     3
<!-- $Id$ -->
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     4
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     5
<html>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     6
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     7
<head>
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
     8
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
     9
  <title>The Isabelle Logo</title>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    10
</head>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    11
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    12
<body>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    13
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    14
<h1>The Isabelle Logo</h1>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    15
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    16
<h2>Versions</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    17
6257
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    18
The logo is available as bitmap file for the generic Isabelle system
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    19
(<a href="#plain">plain</a>, <a href="#transparent">transparent</a>)
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    20
and major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>,
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    21
<a href="#HOLCF">HOLCF</a>).  There are also <a
5243
a0688fa916af added icons;
wenzelm
parents: 4190
diff changeset
    22
href="isabelle-small.xpm">small</a> and <a
a0688fa916af added icons;
wenzelm
parents: 4190
diff changeset
    23
href="isabelle-tiny.xpm">tiny</a> Isabelle icons available.
6257
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    24
Furthermore, scalable (EPS) versions of the logo may be generated for
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    25
any logic using the <tt>isatool logo</tt> utility distributed with
ee0b48ab5aea isatool logo;
wenzelm
parents: 5384
diff changeset
    26
Isabelle.
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    27
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    28
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    29
<h2>Interpretation</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    30
3800
wenzelm
parents: 3799
diff changeset
    31
<img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
3858
wenzelm
parents: 3800
diff changeset
    32
all, the logo tells about the name of the generic system, Isabelle, or
3800
wenzelm
parents: 3799
diff changeset
    33
of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    34
some essentials of the overall Isabelle design philosophy: Composition
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    35
of several small well understood building blocks, grouped together or
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    36
arranged in layers. <p>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    37
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    38
The markings on the cubes illustrate this general principle by example
3800
wenzelm
parents: 3799
diff changeset
    39
of the core meta-logic (which is minimal higher-order logic on top of
wenzelm
parents: 3799
diff changeset
    40
naively polymorphic simply typed lambda calculus). Thus red cubes
7807
wenzelm
parents: 6257
diff changeset
    41
symbolize the type system with function spaces (-&gt;) and type
wenzelm
parents: 6257
diff changeset
    42
variables (alpha); violet ones represent the lambda term language with
wenzelm
parents: 6257
diff changeset
    43
beta conversion etc.; yellow cubes constitute the actual logical
wenzelm
parents: 6257
diff changeset
    44
parts, namely meta-implication or entailment (|-) and meta-level
wenzelm
parents: 6257
diff changeset
    45
universal quantification.
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    46
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    47
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    48
<h2>Acknowledgment</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    49
3858
wenzelm
parents: 3800
diff changeset
    50
The logo is contributed by <a
wenzelm
parents: 3800
diff changeset
    51
href="http://www.informatik.tu-muenchen.de/~wenzel/">Franziska
7807
wenzelm
parents: 6257
diff changeset
    52
Wenzel</a>, Munich.  It has been designed on Apple Macintosh.
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    53
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    54
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    55
<p><hr><p>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    56
3800
wenzelm
parents: 3799
diff changeset
    57
<a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    58
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
    59
<a name="transparent"><img src="isabelle_transparent.gif" alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
    60
black and white displays. <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    61
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
    62
<a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo (ZF)]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    63
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
    64
<a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo (HOL)]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    65
15585
513aa9a3a26d HTML 4.01 Transitional conformity
webertj
parents: 7807
diff changeset
    66
<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo (HOLCF)]"></a>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    67
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    68
</body>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    69
</html>