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