# HG changeset patch # User wenzelm # Date 876220174 -7200 # Node ID d00f6460ac4d63c0b361266acadd105220786a38 # Parent 60ae17f6f37842c235a08fd7012eec875ac1c596 The Isabelle Logo; diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/index.html --- /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 @@ + + + + + + +The Isabelle Logo + + + + +

The Isabelle Logo

+ +

Versions

+ +The logo is available for the generic Isabelle system (plain, transparent) and +major object logics (ZF, HOL, HOLCF). + + +

Interpretation

+ +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.

+ +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. + + +

Acknowledgment

+ +The logo is contributed by Franziska Wenzel, Munich. Thanks +Franziska!

+ + +

+ +Isabelle logo

+ +

+ +Isabelle logo (ZF) +

+ +Isabelle logo +(HOL)

+ +Isabelle logo +(HOLCF)

+ + + diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/isabelle.gif Binary file lib/logo/isabelle.gif has changed diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/isabelle_hol.gif Binary file lib/logo/isabelle_hol.gif has changed diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/isabelle_holcf.gif Binary file lib/logo/isabelle_holcf.gif has changed diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/isabelle_transparent.gif Binary file lib/logo/isabelle_transparent.gif has changed diff -r 60ae17f6f378 -r d00f6460ac4d lib/logo/isabelle_zf.gif Binary file lib/logo/isabelle_zf.gif has changed