lib/logo/index.html
 changeset 3800 5a74678c8645 parent 3799 d00f6460ac4d child 3858 0cfd4f97dd32
equal 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>