updated;

--- a/doc-src/IsarRef/intro.tex	Sat Feb 03 00:01:54 2001 +0100
+++ b/doc-src/IsarRef/intro.tex	Sat Feb 03 00:11:07 2001 +0100
@@ -274,8 +274,7 @@
   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.
+  performed in form of tactic emulation scripts and proper Isar proof texts.
 \end{itemize}