lib/logo/index.html
author haftmann
Sat Apr 26 13:25:44 2014 +0200 (2014-04-26)
changeset 56739 0d56854096ba
parent 33686 8e33ca8832b1
permissions -rw-r--r--
avoid non-standard simp default rule
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <html>
     4 
     5 <head>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     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>isabelle 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" alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
    58 black and white displays. <p>
    59 
    60 <a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo (ZF)]"></a> <p>
    61 
    62 <a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo (HOL)]"></a> <p>
    63 
    64 <a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo (HOLCF)]"></a>
    65 
    66 </body>
    67 </html>