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
+ 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 +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 @@
-
+
+alt="[Isabelle logo (transparent)]">
-
-
+
-
+
-
+