# HG changeset patch
# User wenzelm
# Date 980790997 -3600
# Node ID 883248dcf3f8a0cf94304e635c96dffcc82eeca8
# Parent  0932a82022fde0b0c832a59c035b5f076a897ec2
added Unix example;

diff -r 0932a82022fd -r 883248dcf3f8 doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Mon Jan 29 14:14:17 2001 +0100
+++ b/doc-src/IsarRef/intro.tex	Mon Jan 29 18:56:37 2001 +0100
@@ -255,15 +255,27 @@
   big mathematics application on infinitary vector spaces and functional
   analysis.
 \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
-  properties of $\lambda$-calculus (Church-Rosser and termination).  This may
-  serve as a realistic example of porting of legacy proof scripts into Isar
-  tactic emulation scripts.
+  properties of $\lambda$-calculus (Church-Rosser and termination).
+  
+  This may serve as a realistic example of porting of legacy proof scripts
+  into Isar tactic emulation scripts.
+\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
+  model of the main aspects of the Unix file-system including its security
+  model, but ignoring processes.  A few odd effects caused by the general
+  ``worse-is-better'' approach followed in Unix are discussed within the
+  formal model.
+  
+  This example represents a non-trivial verification task, with all proofs
+  carefully worked out using the proper part of the Isar proof language;
+  unstructured scripts are only used for symbolic evaluation.
 \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
   formalization of a fragment of Java, together with a corresponding virtual
   machine and a specification of its bytecode verifier and a lightweight
-  bytecode verifier, including proofs of type-safety.  This represents a very
-  ``realistic'' example of large formalizations performed in either form of
-  legacy scripts, tactic emulation scripts, and proper Isar proof texts.
+  bytecode verifier, including proofs of type-safety.
+  
+  This represents a very ``realistic'' example of large formalizations
+  performed in either form of legacy scripts, tactic emulation scripts, and
+  proper Isar proof texts.
 \end{itemize}