# HG changeset patch
# User wenzelm
# Date 910037755 -3600
# Node ID 57e3c7775ead6098878ce5090889e65e59ea490b
# Parent 7d4ac02677a6546fa1e61c3f980a15f6c417a626
main Isabelle page;
diff -r 7d4ac02677a6 -r 57e3c7775ead Admin/page/cambridge.gif
Binary file Admin/page/cambridge.gif has changed
diff -r 7d4ac02677a6 -r 57e3c7775ead Admin/page/index.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/index.html Mon Nov 02 21:15:55 1998 +0100
@@ -0,0 +1,139 @@
+
+
+
+
+Isabelle
+
+
+
+Isabelle
![[Isabelle logo]]()
+
+
+
+Isabelle is a popular generic theorem proving
+environment developed at Cambridge University (Larry Paulson) and TU
+Munich (Tobias Nipkow).
+The latest version is Isabelle98-1. It is available
+from several mirror sites.
+
+
+
+Isabelle can be viewed from two main perspectives. On the one hand it
+may serve as a generic framework for rapid prototyping of deductive
+systems. On the other hand, major object logics, like
+Isabelle/HOL, provide a theorem proving environment
+ready to use for sizable applications.
+
+
+
Object logics
+
+The Isabelle distribution includes o large body of object logics and
+other examples (see the Isabelle theory
+library.
+
+
+
+- Isabelle/HOL
-
+is a version of classical higher-order logic, similar to Gordon's HOL
+(it is related to Church's Simple Theory of Types).
+
+
- Isabelle/HOLCF
-
+adds a considerably amount of Scott's domain theory to HOL.
+
+
- Isabelle/FOL
-
+provides basic classical and intuitionistic first-order (polymorphic)
+logic.
+
+
- Isabelle/ZF
-
+offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+
+
+
+
+
+Isabelle/HOL is currently the best developed object logic, including
+an extensive library of (concrete) mathematics, and various packages
+for advanced definitional concepts (like (co-)inductive sets and
+types, well-founded recursion etc.). The distribution also includes
+some large applications, for example correctness proofs of
+cryptographic protocols (HOL/Auth).
+
+
+
+Isabelle/ZF provides another starting point for applications, with a
+slightly less developed library, though. Its definitional packages
+are similar to those of Isabelle/HOL. Untyped ZF provides more
+advanced constructions for sets than simply typed HOL.
+
+
+
+There are also a few minor object logics that may serve as further
+examples: CTT is an
+extensional version of Martin-Löf's Type Theory, Cube is
+Barendregt's Lambda Cube. There are also some sequent calculus
+examples under Sequents,
+including modal or linear logics. There are a few more examples,
+again see the Isabelle theory
+library.
+
+
+
Defining Logics
+
+Logics are not hard-wired into Isabelle, but formulated within
+Isabelle's meta logic: Isabelle/Pure. There are
+quite a lot of syntactic and deductive tools available. Thus defining
+new logics or extending existing ones basically works as follows:
+
+
+
+- declare concrete syntax (via mixfix grammar and syntax macros),
+
+
- declare abstract syntax (as higher-order constants),
+
+
- declare inference rules (as meta-logical propositions),
+
+
- instantiate generic proof tools (simplifier, classical tableau
+prover etc.),
+
+
- manually code special proof procedures (via tacticals or hand
+written ML).
+
+
+
+The first 3 steps are fully declarative and involve no ML programming
+at all. Thus one already gets a decent deductive environment based on
+primitive inferences (by employing the built-in mechanisms of
+Isabelle/Pure, in particular higher-order unification and resolution).
+
+For sizable applications some degree of automated reasoning is
+essential. Instantiating existing tools like the classical tableau
+prover involves only minimal ML based setup. One may also write
+arbitrary proof procedures or even theory extension packages in ML,
+without breaching system soundness (Isabelle follows the well-known
+"LCF system approach").
+
+
+Further information
+
+![[Cambridge]]()
![[Munich]](munich.gif)
The local Isabelle pages at Cambridge
+and Munich provide
+further information on Isabelle and related projects.
+
+
+
diff -r 7d4ac02677a6 -r 57e3c7775ead Admin/page/munich.gif
Binary file Admin/page/munich.gif has changed