--- /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 @@
+
+<html>
+
+<!-- $Id$ -->
+
+<head>
+<title>The Isabelle Logo</title>
+</head>
+
+<body>
+
+<h1>The Isabelle Logo</h1>
+
+<h2>Versions</h2>
+
+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
+href="#HOLCF">HOLCF</a>).
+
+
+<h2>Interpretation</h2>
+
+<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
+quantification.
+
+
+<h2>Acknowledgment</h2>
+
+The logo is contributed by Franziska Wenzel, Munich. Thanks
+Franziska! <p>
+
+
+<p><hr><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>
+
+</body>
+</html>
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
