# HG changeset patch
# User wenzelm
# Date 910038123 -3600
# Node ID 96ab3e0977326885dd1527c20c42e28f2e3ca528
# Parent 57e3c7775ead6098878ce5090889e65e59ea490b
tuned;
diff -r 57e3c7775ead -r 96ab3e097732 Admin/page/index.html
--- a/Admin/page/index.html Mon Nov 02 21:15:55 1998 +0100
+++ b/Admin/page/index.html Mon Nov 02 21:22:03 1998 +0100
@@ -1,4 +1,3 @@
-
@@ -22,17 +21,17 @@
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
+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
+The Isabelle distribution includes a large body of object logics and
other examples (see the Isabelle theory
-library.
+library).
@@ -93,8 +92,9 @@
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:
+quite a lot of syntactic and deductive tools available in generic
+Isabelle. Thus defining new logics or extending existing ones
+basically works as follows:
@@ -112,17 +112,18 @@
-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).
+The first 3 steps above 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
+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").
+"LCF system approach" to achieve a secure system).
Further information
@@ -135,5 +136,4 @@
and Munich provide
further information on Isabelle and related projects.
-