author wenzelm
Tue, 07 Oct 1997 12:37:53 +0200
changeset 3800 5a74678c8645
parent 3799 d00f6460ac4d
child 3858 0cfd4f97dd32
permissions -rw-r--r--


<!-- $Id$ -->

<title>The Isabelle Logo</title>


<h1>The Isabelle Logo</h1>


The logo is available for the generic Isabelle system (<a
href="#plain">plain</a>, <a href="#transparent">transparent</a>) and
major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>, <a


<img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
all the logo tells about the name of the generic system, Isabelle, or
of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
some essentials of the overall Isabelle design philosophy: Composition
of several small well understood building blocks, grouped together or
arranged in layers. <p>

The markings on the cubes illustrate this general principle by example
of the core meta-logic (which is minimal higher-order logic on top of
naively polymorphic simply typed lambda calculus). Thus red cubes
symbolize the type system with function spaces (->) and type variables
(alpha); violet ones represent the lambda term language with beta
conversion etc.; yellow cubes constitute the actual logical parts,
namely meta-implication or entailment (|-) and meta-level universal


The logo is contributed by Franziska Wenzel, Munich.  Thanks
Franziska! <p>


<a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>

<a name="transparent"><img src="isabelle_transparent.gif"
alt="[Isabelle logo (transparent)]"></a> <p>

<a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo
(ZF)]"></a> <p>

<a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo
(HOL)]"></a> <p>

<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
(HOLCF)]"></a> <p>