# HG changeset patch
# User wenzelm
# Date 981155467 -3600
# Node ID e07b601e2b5a465280eb9869747d0e6e3c22b03b
# Parent  194406da4e43a902dcc4dc4a6325890ca057ca46
updated;

diff -r 194406da4e43 -r e07b601e2b5a doc-src/IsarRef/intro.tex
--- 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}