# 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}