lib/logo/index.html
changeset 3800 5a74678c8645
parent 3799 d00f6460ac4d
child 3858 0cfd4f97dd32
equal deleted inserted replaced
3799:d00f6460ac4d 3800:5a74678c8645
    19 href="#HOLCF">HOLCF</a>).
    19 href="#HOLCF">HOLCF</a>).
    20 
    20 
    21 
    21 
    22 <h2>Interpretation</h2>
    22 <h2>Interpretation</h2>
    23 
    23 
    24 <img src="isabelle.gif" align=right alt="Isabelle logo"> First of all
    24 <img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
    25 the logo tells about the name of the generic system, Isabelle, or of
    25 all the logo tells about the name of the generic system, Isabelle, or
    26 its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
    26 of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
    27 some essentials of the overall Isabelle design philosophy: Composition
    27 some essentials of the overall Isabelle design philosophy: Composition
    28 of several small well understood building blocks, grouped together or
    28 of several small well understood building blocks, grouped together or
    29 arranged in layers. <p>
    29 arranged in layers. <p>
    30 
    30 
    31 The markings on the cubes illustrate this general principle by example
    31 The markings on the cubes illustrate this general principle by example
    32 of the core meta-logic (which is naively polymorphic simply typed
    32 of the core meta-logic (which is minimal higher-order logic on top of
    33 lambda calculus with minimal higher-order logic). Thus red cubes
    33 naively polymorphic simply typed lambda calculus). Thus red cubes
    34 symbolize the type system with function spaces (->) and type variables
    34 symbolize the type system with function spaces (->) and type variables
    35 (alpha); violet ones represent the lambda term language with beta
    35 (alpha); violet ones represent the lambda term language with beta
    36 conversion etc.; yellow cubes constitute the actual logical parts,
    36 conversion etc.; yellow cubes constitute the actual logical parts,
    37 namely meta-implication or entailment (|-) and meta-level universal
    37 namely meta-implication or entailment (|-) and meta-level universal
    38 quantification.
    38 quantification.
    44 Franziska! <p>
    44 Franziska! <p>
    45 
    45 
    46 
    46 
    47 <p><hr><p>
    47 <p><hr><p>
    48 
    48 
    49 <a name="plain"><img src="isabelle.gif" alt="Isabelle logo"></a> <p>
    49 <a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>
    50 
    50 
    51 <a name="transparent"><img src="isabelle_transparent.gif"
    51 <a name="transparent"><img src="isabelle_transparent.gif"
    52 alt="Isabelle logo (transparent)"></a> <p>
    52 alt="[Isabelle logo (transparent)]"></a> <p>
    53 
    53 
    54 <a name="ZF"><img src="isabelle_zf.gif" alt="Isabelle logo (ZF)"></a>
    54 <a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo
    55 <p>
    55 (ZF)]"></a> <p>
    56 
    56 
    57 <a name="HOL"><img src="isabelle_hol.gif" alt="Isabelle logo
    57 <a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo
    58 (HOL)"></a> <p>
    58 (HOL)]"></a> <p>
    59 
    59 
    60 <a name="HOLCF"><img src="isabelle_holcf.gif" alt="Isabelle logo
    60 <a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
    61 (HOLCF)"></a> <p>
    61 (HOLCF)]"></a> <p>
    62 
    62 
    63 </body>
    63 </body>
    64 </html>
    64 </html>