lib/logo/index.html
author oheimb
Tue, 07 Apr 1998 13:46:05 +0200
changeset 4800 97c3a45d092b
parent 4190 e377947fe1ec
child 5243 a0688fa916af
permissions -rw-r--r--
replaced option_map_SomeD by option_map_eq_Some (RS iffD1) added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     1
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     2
<html>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     3
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     4
<!-- $Id$ -->
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     5
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     6
<head>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     7
<title>The Isabelle Logo</title>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     8
</head>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
     9
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    10
<body>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    11
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    12
<h1>The Isabelle Logo</h1>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    13
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    14
<h2>Versions</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    15
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    16
The logo is available for the generic Isabelle system (<a
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    17
href="#plain">plain</a>, <a href="#transparent">transparent</a>) and
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    18
major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>, <a
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    19
href="#HOLCF">HOLCF</a>).
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    20
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    21
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    22
<h2>Interpretation</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    23
3800
wenzelm
parents: 3799
diff changeset
    24
<img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
3858
wenzelm
parents: 3800
diff changeset
    25
all, the logo tells about the name of the generic system, Isabelle, or
3800
wenzelm
parents: 3799
diff changeset
    26
of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    27
some essentials of the overall Isabelle design philosophy: Composition
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    28
of several small well understood building blocks, grouped together or
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    29
arranged in layers. <p>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    30
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    31
The markings on the cubes illustrate this general principle by example
3800
wenzelm
parents: 3799
diff changeset
    32
of the core meta-logic (which is minimal higher-order logic on top of
wenzelm
parents: 3799
diff changeset
    33
naively polymorphic simply typed lambda calculus). Thus red cubes
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    34
symbolize the type system with function spaces (->) and type variables
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    35
(alpha); violet ones represent the lambda term language with beta
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    36
conversion etc.; yellow cubes constitute the actual logical parts,
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    37
namely meta-implication or entailment (|-) and meta-level universal
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    38
quantification.
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    39
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    40
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    41
<h2>Acknowledgment</h2>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    42
3858
wenzelm
parents: 3800
diff changeset
    43
The logo is contributed by <a
wenzelm
parents: 3800
diff changeset
    44
href="http://www.informatik.tu-muenchen.de/~wenzel/">Franziska
4190
e377947fe1ec fixed spelling;
wenzelm
parents: 3858
diff changeset
    45
Wenzel</a>, Munich.  It has been designed on Apple Macintosh. <p>
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
<p><hr><p>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    49
3800
wenzelm
parents: 3799
diff changeset
    50
<a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    51
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    52
<a name="transparent"><img src="isabelle_transparent.gif"
3858
wenzelm
parents: 3800
diff changeset
    53
alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
wenzelm
parents: 3800
diff changeset
    54
black and white displays.  <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    55
3800
wenzelm
parents: 3799
diff changeset
    56
<a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo
wenzelm
parents: 3799
diff changeset
    57
(ZF)]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    58
3800
wenzelm
parents: 3799
diff changeset
    59
<a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo
wenzelm
parents: 3799
diff changeset
    60
(HOL)]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    61
3800
wenzelm
parents: 3799
diff changeset
    62
<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
wenzelm
parents: 3799
diff changeset
    63
(HOLCF)]"></a> <p>
3799
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    64
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    65
</body>
d00f6460ac4d The Isabelle Logo;
wenzelm
parents:
diff changeset
    66
</html>