author wenzelm Tue, 07 Oct 1997 12:37:53 +0200 changeset 3800 5a74678c8645 parent 3799 d00f6460ac4d child 3801 5ba459e15dd7
tuned;
 lib/logo/index.html file | annotate | diff | comparison | revisions
```--- a/lib/logo/index.html	Tue Oct 07 12:29:34 1997 +0200
+++ b/lib/logo/index.html	Tue Oct 07 12:37:53 1997 +0200
@@ -21,16 +21,16 @@

<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
+<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
+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,
@@ -46,19 +46,19 @@

<p><hr><p>

-<a name="plain"><img src="isabelle.gif" alt="Isabelle logo"></a> <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>
+alt="[Isabelle logo (transparent)]"></a> <p>

-<a name="ZF"><img src="isabelle_zf.gif" alt="Isabelle logo (ZF)"></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="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>
+<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
+(HOLCF)]"></a> <p>

</body>
</html>```