The Isabelle Logo;
Tue, 07 Oct 1997 12:29:34 +0200
changeset 3799 d00f6460ac4d
parent 3798 60ae17f6f378
child 3800 5a74678c8645
The Isabelle Logo;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/logo/index.html	Tue Oct 07 12:29:34 1997 +0200
@@ -0,0 +1,64 @@
+<!-- $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 naively polymorphic simply typed
+lambda calculus with minimal higher-order logic). 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>
+<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>
Binary file lib/logo/isabelle.gif has changed
Binary file lib/logo/isabelle_hol.gif has changed
Binary file lib/logo/isabelle_holcf.gif has changed
Binary file lib/logo/isabelle_transparent.gif has changed
Binary file lib/logo/isabelle_zf.gif has changed