lib/logo/index.html
author wenzelm
Fri Oct 05 21:52:39 2001 +0200 (2001-10-05)
changeset 11701 3d51fbf81c17
parent 7807 6a102f74ad0a
child 15585 513aa9a3a26d
permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
     1 
     2 <html>
     3 
     4 <!-- $Id$ -->
     5 
     6 <head>
     7 <title>The Isabelle Logo</title>
     8 </head>
     9 
    10 <body>
    11 
    12 <h1>The Isabelle Logo</h1>
    13 
    14 <h2>Versions</h2>
    15 
    16 The logo is available as bitmap file for the generic Isabelle system
    17 (<a href="#plain">plain</a>, <a href="#transparent">transparent</a>)
    18 and major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>,
    19 <a href="#HOLCF">HOLCF</a>).  There are also <a
    20 href="isabelle-small.xpm">small</a> and <a
    21 href="isabelle-tiny.xpm">tiny</a> Isabelle icons available.
    22 Furthermore, scalable (EPS) versions of the logo may be generated for
    23 any logic using the <tt>isatool logo</tt> utility distributed with
    24 Isabelle.
    25 
    26 
    27 <h2>Interpretation</h2>
    28 
    29 <img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
    30 all, the logo tells about the name of the generic system, Isabelle, or
    31 of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
    32 some essentials of the overall Isabelle design philosophy: Composition
    33 of several small well understood building blocks, grouped together or
    34 arranged in layers. <p>
    35 
    36 The markings on the cubes illustrate this general principle by example
    37 of the core meta-logic (which is minimal higher-order logic on top of
    38 naively polymorphic simply typed lambda calculus). Thus red cubes
    39 symbolize the type system with function spaces (-&gt;) and type
    40 variables (alpha); violet ones represent the lambda term language with
    41 beta conversion etc.; yellow cubes constitute the actual logical
    42 parts, namely meta-implication or entailment (|-) and meta-level
    43 universal quantification.
    44 
    45 
    46 <h2>Acknowledgment</h2>
    47 
    48 The logo is contributed by <a
    49 href="http://www.informatik.tu-muenchen.de/~wenzel/">Franziska
    50 Wenzel</a>, Munich.  It has been designed on Apple Macintosh.
    51 
    52 
    53 <p><hr><p>
    54 
    55 <a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>
    56 
    57 <a name="transparent"><img src="isabelle_transparent.gif"
    58 alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
    59 black and white displays.  <p>
    60 
    61 <a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo
    62 (ZF)]"></a> <p>
    63 
    64 <a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo
    65 (HOL)]"></a> <p>
    66 
    67 <a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
    68 (HOLCF)]"></a>
    69 
    70 </body>
    71 </html>